From f53f226f5504dc4b3d706bab09e36588a3d69149 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 17 Sep 2024 03:13:36 +0200
Subject: [PATCH] remove module wraps in each file

---
 coq/context.v   |  6 ------
 coq/equiv.v     |  9 ---------
 coq/morph.v     | 11 -----------
 coq/smallstep.v |  9 +--------
 coq/soundness.v | 14 ++------------
 coq/subst.v     |  6 ------
 coq/subtype.v   |  6 ------
 coq/terms.v     |  3 ---
 coq/typing.v    |  9 ---------
 9 files changed, 3 insertions(+), 70 deletions(-)

diff --git a/coq/context.v b/coq/context.v
index 549af74..88e8cc3 100644
--- a/coq/context.v
+++ b/coq/context.v
@@ -1,8 +1,5 @@
 From Coq Require Import Strings.String.
 Require Import terms.
-Include Terms.
-
-Module Context.
 
 
 Inductive context : Type :=
@@ -16,6 +13,3 @@ Inductive context_contains : context -> string -> type_term -> Prop :=
   | C_shuffle : forall x X y Y Γ,
     (context_contains Γ x X) ->
     (context_contains (ctx_assign y Y Γ) x X).
-
-
-End Context.
diff --git a/coq/equiv.v b/coq/equiv.v
index 603ec86..7ed4272 100644
--- a/coq/equiv.v
+++ b/coq/equiv.v
@@ -34,12 +34,6 @@ Require Import terms.
 Require Import subst.
 From Coq Require Import Strings.String.
 
-Include Terms.
-Include Subst.
-
-Module Equiv.
-
-
 (** Alpha conversion in types *)
 
 Reserved Notation "S '--->α' T" (at level 40).
@@ -407,6 +401,3 @@ Proof.
   apply TEq_Distribute.
   apply L_DistributeOverSpec2.
 Qed.
-
-
-End Equiv.
diff --git a/coq/morph.v b/coq/morph.v
index 9746a61..a686102 100644
--- a/coq/morph.v
+++ b/coq/morph.v
@@ -5,14 +5,6 @@ Require Import equiv.
 Require Import subtype.
 Require Import context.
 
-Include Terms.
-Include Subst.
-Include Equiv.
-Include Subtype.
-Include Context.
-
-Module Morph.
-
 (* Given a context, there is a morphism path from τ to τ' *)
 Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
 
@@ -97,6 +89,3 @@ Proof.
   apply C_shuffle.
   apply C_take.
 Qed.
-
-
-End Morph.
diff --git a/coq/smallstep.v b/coq/smallstep.v
index 16d45c9..d5cb87b 100644
--- a/coq/smallstep.v
+++ b/coq/smallstep.v
@@ -1,14 +1,9 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import subst.
+Require Import subtype.
 Require Import typing.
 
-Include Terms.
-Include Subst.
-Include Typing.
-
-Module Smallstep.
-
 Reserved Notation " s '-->α' t " (at level 40).
 Reserved Notation " s '-->β' t " (at level 40).
 
@@ -140,5 +135,3 @@ Proof.
 
   apply Multi_Refl.
 Qed.
-
-End Smallstep.
diff --git a/coq/soundness.v b/coq/soundness.v
index 0d47ec4..d121044 100644
--- a/coq/soundness.v
+++ b/coq/soundness.v
@@ -3,19 +3,11 @@ Require Import terms.
 Require Import subst.
 Require Import equiv.
 Require Import subtype.
+Require Import context.
+Require Import morph.
 Require Import smallstep.
 Require Import typing.
 
-Include Terms.
-Include Subst.
-Include Equiv.
-Include Subtype.
-Include Smallstep.
-Include Typing.
-
-
-Module Soundness.
-
 
 Lemma typing_weakening : forall Γ e τ x σ,
   (Γ |- e \is τ) ->
@@ -414,5 +406,3 @@ Proof.
   admit.
 Admitted.
 
-End Soundness.
-
diff --git a/coq/subst.v b/coq/subst.v
index 02eb711..7cb13fc 100644
--- a/coq/subst.v
+++ b/coq/subst.v
@@ -1,10 +1,6 @@
  From Coq Require Import Strings.String.
 Require Import terms.
 
-Include Terms.
-
-Module Subst.
-
 (* Type Variable "x" is a free variable in type *)
 Inductive type_var_free (x:string) : type_term -> Prop :=
   | TFree_Var :
@@ -128,5 +124,3 @@ Fixpoint expr_specialize (v:string) (n:type_term) (e0:expr_term) :=
   | expr_descend t e => expr_descend (type_subst v n t) (expr_specialize v n e)
   | e => e
   end.
-
-End Subst.
diff --git a/coq/subtype.v b/coq/subtype.v
index 5ffd0be..afaacd0 100644
--- a/coq/subtype.v
+++ b/coq/subtype.v
@@ -11,10 +11,6 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import equiv.
-Include Terms.
-Include Equiv.
-
-Module Subtype.
 
 (** Subtyping *)
 
@@ -96,5 +92,3 @@ Proof.
 	apply TSubRepr_Refl.
 	apply TEq_Refl.
 Qed.
-
-End Subtype.
diff --git a/coq/terms.v b/coq/terms.v
index a60a2c1..00c075d 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -4,7 +4,6 @@
  *)
 
 From Coq Require Import Strings.String.
-Module Terms.
 
 (* types *)
 Inductive type_term : Type :=
@@ -118,5 +117,3 @@ Compute polymorphic_identity1.
 
 Close Scope ladder_type_scope.
 Close Scope ladder_expr_scope.
-
-End Terms.
diff --git a/coq/typing.v b/coq/typing.v
index 2430ac1..34710c7 100644
--- a/coq/typing.v
+++ b/coq/typing.v
@@ -9,15 +9,6 @@ Require Import subtype.
 Require Import context.
 Require Import morph.
 
-Include Terms.
-Include Subst.
-Include Equiv.
-Include Subtype.
-Include Context.
-Include Morph.
-
-Module Typing.
-
 (** Typing Derivation *)
 
 Reserved Notation "Gamma '|-' x '\is' X"  (at level 101, x at next level, X at level 0).