diff options
Diffstat (limited to 'test-suite/success/Mod_strengthen.v')
| -rw-r--r-- | test-suite/success/Mod_strengthen.v | 49 |
1 files changed, 26 insertions, 23 deletions
diff --git a/test-suite/success/Mod_strengthen.v b/test-suite/success/Mod_strengthen.v index a472e698..449610be 100644 --- a/test-suite/success/Mod_strengthen.v +++ b/test-suite/success/Mod_strengthen.v @@ -1,25 +1,27 @@ Module Type Sub. - Axiom Refl1 : (x:nat)(x=x). - Axiom Refl2 : (x:nat)(x=x). - Axiom Refl3 : (x:nat)(x=x). - Inductive T : Set := A : T. + Axiom Refl1 : forall x : nat, x = x. + Axiom Refl2 : forall x : nat, x = x. + Axiom Refl3 : forall x : nat, x = x. + Inductive T : Set := + A : T. End Sub. Module Type Main. - Declare Module M:Sub. + Declare Module M: Sub. End Main. Module A <: Main. Module M <: Sub. - Lemma Refl1 : (x:nat) x=x. - Intros;Reflexivity. + Lemma Refl1 : forall x : nat, x = x. + intros; reflexivity. Qed. - Axiom Refl2 : (x:nat) x=x. - Lemma Refl3 : (x:nat) x=x. - Intros;Reflexivity. + Axiom Refl2 : forall x : nat, x = x. + Lemma Refl3 : forall x : nat, x = x. + intros; reflexivity. Defined. - Inductive T : Set := A : T. + Inductive T : Set := + A : T. End M. End A. @@ -27,8 +29,8 @@ End A. (* first test *) -Module F[S:Sub]. - Module M:=S. +Module F (S: Sub). + Module M := S. End F. Module B <: Main with Module M:=A.M := F A.M. @@ -37,28 +39,29 @@ Module B <: Main with Module M:=A.M := F A.M. (* second test *) -Lemma r1 : (A.M.Refl1 == B.M.Refl1). +Lemma r1 : (A.M.Refl1 = B.M.Refl1). Proof. - Reflexivity. + reflexivity. Qed. -Lemma r2 : (A.M.Refl2 == B.M.Refl2). +Lemma r2 : (A.M.Refl2 = B.M.Refl2). Proof. - Reflexivity. + reflexivity. Qed. -Lemma r3 : (A.M.Refl3 == B.M.Refl3). +Lemma r3 : (A.M.Refl3 = B.M.Refl3). Proof. - Reflexivity. + reflexivity. Qed. -Lemma t : (A.M.T == B.M.T). +Lemma t : (A.M.T = B.M.T). Proof. - Reflexivity. + reflexivity. Qed. -Lemma a : (A.M.A == B.M.A). +Lemma a : (A.M.A = B.M.A). Proof. - Reflexivity. + reflexivity. Qed. + |