diff options
Diffstat (limited to 'test-suite/modules')
-rw-r--r-- | test-suite/modules/PO.v | 8 | ||||
-rw-r--r-- | test-suite/modules/Przyklad.v | 24 | ||||
-rw-r--r-- | test-suite/modules/Tescik.v | 6 | ||||
-rw-r--r-- | test-suite/modules/fun_objects.v | 2 | ||||
-rw-r--r-- | test-suite/modules/injection_discriminate_inversion.v | 20 | ||||
-rw-r--r-- | test-suite/modules/mod_decl.v | 10 | ||||
-rw-r--r-- | test-suite/modules/modeq.v | 2 | ||||
-rw-r--r-- | test-suite/modules/modul.v | 2 | ||||
-rw-r--r-- | test-suite/modules/obj.v | 2 | ||||
-rw-r--r-- | test-suite/modules/objects.v | 2 | ||||
-rw-r--r-- | test-suite/modules/objects2.v | 2 | ||||
-rw-r--r-- | test-suite/modules/sig.v | 4 | ||||
-rw-r--r-- | test-suite/modules/sub_objects.v | 2 | ||||
-rw-r--r-- | test-suite/modules/subtyping.v | 8 |
14 files changed, 47 insertions, 47 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 354c3957..71d33177 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -7,11 +7,11 @@ Implicit Arguments snd. Module Type PO. Parameter T : Set. Parameter le : T -> T -> Prop. - + Axiom le_refl : forall x : T, le x x. Axiom le_trans : forall x y z : T, le x y -> le y z -> le x z. Axiom le_antis : forall x y : T, le x y -> le y x -> x = y. - + Hint Resolve le_refl le_trans le_antis. End PO. @@ -28,10 +28,10 @@ Module Pair (X: PO) (Y: PO) <: PO. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. unfold le in |- *; intuition; info eauto. - Qed. + Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. - destruct p1. + destruct p1. destruct p2. unfold le in |- *. intuition. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 014f6c60..e3694b81 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,4 +1,4 @@ -Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) +Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) (th el : T) := if s then th else el. Implicit Arguments ifte. @@ -33,7 +33,7 @@ Module Type ELEM. Parameter T : Set. Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}. End ELEM. - + Module Type SET (Elt: ELEM). Parameter T : Set. Parameter empty : T. @@ -104,11 +104,11 @@ Module Nat. End Nat. -Module SetNat := F Nat. +Module SetNat := F Nat. -Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. -apply SetNat.find_empty_false. +Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. +apply SetNat.find_empty_false. Qed. (***************************************************************************) @@ -120,8 +120,8 @@ Module Lemmas (G: SET) (E: ELEM). forall (S : ESet.T) (a1 a2 : E.T), let S1 := ESet.add a1 (ESet.add a2 S) in let S2 := ESet.add a2 (ESet.add a1 S) in - forall a : E.T, ESet.find a S1 = ESet.find a S2. - + forall a : E.T, ESet.find a S1 = ESet.find a S2. + intros. unfold S1, S2 in |- *. elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2; @@ -137,10 +137,10 @@ Inductive list (A : Set) : Set := | nil : list A | cons : A -> list A -> list A. -Module ListDict (E: ELEM). +Module ListDict (E: ELEM). Definition T := list E.T. Definition elt := E.T. - + Definition empty := nil elt. Definition add (e : elt) (s : T) := cons elt e s. Fixpoint find (e : elt) (s : T) {struct s} : bool := @@ -160,7 +160,7 @@ Module ListDict (E: ELEM). auto. Qed. - + Lemma find_add_false : forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. @@ -171,8 +171,8 @@ Module ListDict (E: ELEM). rewrite H0. simpl in |- *. reflexivity. - Qed. - + Qed. + End ListDict. diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v index 8dadace7..1d1b1e0a 100644 --- a/test-suite/modules/Tescik.v +++ b/test-suite/modules/Tescik.v @@ -7,20 +7,20 @@ End ELEM. Module Nat. Definition A := nat. Definition x := 0. -End Nat. +End Nat. Module List (X: ELEM). Inductive list : Set := | nil : list | cons : X.A -> list -> list. - + Definition head (l : list) := match l with | nil => X.x | cons x _ => x end. Definition singl (x : X.A) := cons x nil. - + Lemma head_singl : forall x : X.A, head (singl x) = x. auto. Qed. diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v index f4dc19b3..dce2ffd5 100644 --- a/test-suite/modules/fun_objects.v +++ b/test-suite/modules/fun_objects.v @@ -4,7 +4,7 @@ Unset Strict Implicit. Module Type SIG. Parameter id : forall A : Set, A -> A. End SIG. - + Module M (X: SIG). Definition idid := X.id X.id. Definition id := idid X.id. diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v index 88c19cb1..d4ac7b3a 100644 --- a/test-suite/modules/injection_discriminate_inversion.v +++ b/test-suite/modules/injection_discriminate_inversion.v @@ -7,18 +7,18 @@ Module M1 := M. Goal forall x, M.C x = M1.C 0 -> x = 0 . intros x H. - (* - injection sur deux constructeurs egaux mais appeles - par des modules differents + (* + injection sur deux constructeurs egaux mais appeles + par des modules differents *) - injection H. + injection H. tauto. Qed. Goal M.C 0 <> M1.C 1. - (* - Discriminate sur deux constructeurs egaux mais appeles - par des modules differents + (* + Discriminate sur deux constructeurs egaux mais appeles + par des modules differents *) intro H;discriminate H. Qed. @@ -26,9 +26,9 @@ Qed. Goal forall x, M.C x = M1.C 0 -> x = 0. intros x H. - (* - inversion sur deux constructeurs egaux mais appeles - par des modules differents + (* + inversion sur deux constructeurs egaux mais appeles + par des modules differents *) inversion H. reflexivity. Qed.
\ No newline at end of file diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v index b886eb59..8b40213a 100644 --- a/test-suite/modules/mod_decl.v +++ b/test-suite/modules/mod_decl.v @@ -31,17 +31,17 @@ Module Type T. Module M0. Axiom A : Set. End M0. - + Declare Module M1: SIG. - + Module M2 <: SIG. Definition A := nat. End M2. - + Module M3 := M0. - + Module M4 : SIG := M0. - + Module M5 <: SIG := M0. Module M6 := F M0. diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v index 45cf9f12..1238ee9d 100644 --- a/test-suite/modules/modeq.v +++ b/test-suite/modules/modeq.v @@ -19,4 +19,4 @@ Module Z. Module N := M. End Z. -Module A : SIG := Z.
\ No newline at end of file +Module A : SIG := Z.
\ No newline at end of file diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v index 9d24d6ce..36a542ef 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -6,7 +6,7 @@ Module M. Hint Resolve w. (* <Warning> : Grammar is replaced by Notation *) - + Print Hint *. Lemma w1 : rel 0 1. diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v index 97337a12..fda1a074 100644 --- a/test-suite/modules/obj.v +++ b/test-suite/modules/obj.v @@ -1,7 +1,7 @@ Set Implicit Arguments. Unset Strict Implicit. -Module M. +Module M. Definition a (s : Set) := s. Print a. End M. diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v index 070f859e..d3a4c0b0 100644 --- a/test-suite/modules/objects.v +++ b/test-suite/modules/objects.v @@ -2,7 +2,7 @@ Module Type SET. Axiom T : Set. Axiom x : T. End SET. - + Set Implicit Arguments. Unset Strict Implicit. diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v index e286609e..220e2b36 100644 --- a/test-suite/modules/objects2.v +++ b/test-suite/modules/objects2.v @@ -4,7 +4,7 @@ (* Bug #1118 (simplified version), submitted by Evelyne Contejean (used to failed in pre-V8.1 trunk because of a call to lookup_mind - for structure objects) + for structure objects) *) Module Type S. Record t : Set := { a : nat; b : nat }. End S. diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v index 4cb6291d..da5d25fa 100644 --- a/test-suite/modules/sig.v +++ b/test-suite/modules/sig.v @@ -18,8 +18,8 @@ Module Type SPRYT. End N. End SPRYT. -Module K : SPRYT := N. -Module K' : SPRYT := M. +Module K : SPRYT := N. +Module K' : SPRYT := M. Module Type SIG. Definition T : Set := M.N.T. diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v index 5eec0775..fdfd09f8 100644 --- a/test-suite/modules/sub_objects.v +++ b/test-suite/modules/sub_objects.v @@ -12,7 +12,7 @@ Module M. Module N. Definition idid (A : Set) (x : A) := id x. (* <Warning> : Grammar is replaced by Notation *) - Notation inc := (plus 1). + Notation inc := (plus 1). End N. Definition zero := N.idid 0. diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v index 2df8e84e..dd7daf42 100644 --- a/test-suite/modules/subtyping.v +++ b/test-suite/modules/subtyping.v @@ -15,7 +15,7 @@ Module Type T. Parameter A : Type (* Top.1 *) . - Inductive L : Type (* max(Top.1,1) *) := + Inductive L : Type (* max(Top.1,1) *) := | L0 | L1 : (A -> Prop) -> L. @@ -23,17 +23,17 @@ End T. Axiom Tp : Type (* Top.5 *) . -Module TT : T. +Module TT : T. Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *) - Inductive L : Type (* max(Top.6,1) *) := + Inductive L : Type (* max(Top.6,1) *) := | L0 | L1 : (A -> Prop) -> L. End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *) -(* Note: Top.6 <= Top.1 is generated by subtyping on A; +(* Note: Top.6 <= Top.1 is generated by subtyping on A; subtyping of L follows and has not to be checked *) |