From 4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 21 Dec 2005 23:50:17 +0000 Subject: Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/modules/Demo.v | 32 +++--- test-suite/modules/Nat.v | 22 ++-- test-suite/modules/PO.v | 64 +++++------ test-suite/modules/Przyklad.v | 226 +++++++++++++++++++-------------------- test-suite/modules/Tescik.v | 32 +++--- test-suite/modules/fun_objects.v | 28 ++--- test-suite/modules/grammar.v | 22 ++-- test-suite/modules/ind.v | 18 ++-- test-suite/modules/mod_decl.v | 40 +++---- test-suite/modules/modeq.v | 18 ++-- test-suite/modules/modul.v | 26 +++-- test-suite/modules/obj.v | 12 +-- test-suite/modules/objects.v | 28 ++--- test-suite/modules/pliczek.v | 2 +- test-suite/modules/plik.v | 5 +- test-suite/modules/sig.v | 26 ++--- test-suite/modules/sub_objects.v | 27 +++-- 17 files changed, 311 insertions(+), 317 deletions(-) (limited to 'test-suite/modules') diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v index 1e9273f07..1f27fe1ba 100644 --- a/test-suite/modules/Demo.v +++ b/test-suite/modules/Demo.v @@ -1,51 +1,51 @@ Module M. - Definition t:=nat. - Definition x:=O. + Definition t := nat. + Definition x := 0. End M. Print M.t. Module Type SIG. - Parameter t:Set. - Parameter x:t. + Parameter t : Set. + Parameter x : t. End SIG. -Module F[X:SIG]. - Definition t:=X.t->X.t. - Definition x:t. - Intro. - Exact X.x. +Module F (X: SIG). + Definition t := X.t -> X.t. + Definition x : t. + intro. + exact X.x. Defined. - Definition y:=X.x. + Definition y := X.x. End F. Module N := F M. Print N.t. -Eval Compute in N.t. +Eval compute in N.t. Module N' : SIG := N. Print N'.t. -Eval Compute in N'.t. +Eval compute in N'.t. Module N'' <: SIG := F N. Print N''.t. -Eval Compute in N''.t. +Eval compute in N''.t. -Eval Compute in N''.x. +Eval compute in N''.x. -Module N''' : SIG with Definition t:=nat->nat := N. +Module N''' : SIG with Definition t := nat -> nat := N. Print N'''.t. -Eval Compute in N'''.t. +Eval compute in N'''.t. Print N'''.x. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index d3e98ae4d..57878a5f1 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -1,19 +1,19 @@ -Definition T:=nat. +Definition T := nat. -Definition le:=Peano.le. +Definition le := le. -Hints Unfold le. +Hint Unfold le. -Lemma le_refl:(n:nat)(le n n). - Auto. +Lemma le_refl : forall n : nat, le n n. + auto. Qed. -Require Le. +Require Import Le. -Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k). - EAuto with arith. +Lemma le_trans : forall n m k : nat, le n m -> le m k -> le n k. + eauto with arith. Qed. -Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m. - EAuto with arith. -Qed. +Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m. + eauto with arith. +Qed. \ No newline at end of file diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 9ba3fb2e6..354c3957f 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -1,57 +1,57 @@ -Implicit Arguments On. +Set Implicit Arguments. +Unset Strict Implicit. -Implicits fst. -Implicits snd. +Implicit Arguments fst. +Implicit Arguments snd. Module Type PO. - Parameter T:Set. - Parameter le:T->T->Prop. + Parameter T : Set. + Parameter le : T -> T -> Prop. - Axiom le_refl : (x:T)(le x x). - Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z). - Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y). + 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. - Hints Resolve le_refl le_trans le_antis. + Hint Resolve le_refl le_trans le_antis. End PO. -Module Pair[X:PO][Y:PO] <: PO. - Definition T:=X.T*Y.T. - Definition le:=[p1,p2] - (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)). +Module Pair (X: PO) (Y: PO) <: PO. + Definition T := (X.T * Y.T)%type. + Definition le p1 p2 := X.le (fst p1) (fst p2) /\ Y.le (snd p1) (snd p2). - Hints Unfold le. + Hint Unfold le. - Lemma le_refl : (p:T)(le p p). - Info Auto. + Lemma le_refl : forall p : T, le p p. + info auto. Qed. - Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3). - Unfold le; Intuition; Info EAuto. + Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. + unfold le in |- *; intuition; info eauto. Qed. - Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2). - NewDestruct p1. - NewDestruct p2. - Unfold le. - Intuition. - CutRewrite t=t1. - CutRewrite t0=t2. - Reflexivity. + Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. + destruct p1. + destruct p2. + unfold le in |- *. + intuition. + cutrewrite (t = t1). + cutrewrite (t0 = t2). + reflexivity. - Info Auto. + info auto. - Info Auto. + info auto. Qed. End Pair. -Read Module Nat. +Require Nat. Module NN := Pair Nat Nat. -Lemma zz_min : (p:NN.T)(NN.le (O,O) p). - Info Auto with arith. -Qed. +Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. + info auto with arith. +Qed. \ No newline at end of file diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 4f4c2066d..014f6c604 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,38 +1,40 @@ -Definition ifte := [T:Set][A:Prop][B:Prop][s:(sumbool A B)][th:T][el:T] - if s then [_]th else [_]el. +Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) + (th el : T) := if s then th else el. -Implicits ifte. +Implicit Arguments ifte. -Lemma Reflexivity_provable : - (A:Set)(a:A)(s:{a=a}+{~a=a})(EXT x| s==(left ? ? x)). -Intros. -Elim s. -Intro x. -Split with x; Reflexivity. +Lemma Reflexivity_provable : + forall (A : Set) (a : A) (s : {a = a} + {a <> a}), + exists x : _, s = left _ x. +intros. +elim s. +intro x. +split with x; reflexivity. -Intro. -Absurd a=a; Auto. +intro. + absurd (a = a); auto. -Save. +Qed. -Lemma Disequality_provable : - (A:Set)(a,b:A)(~a=b)->(s:{a=b}+{~a=b})(EXT x| s==(right ? ? x)). -Intros. -Elim s. -Intro. -Absurd a=a; Auto. +Lemma Disequality_provable : + forall (A : Set) (a b : A), + a <> b -> forall s : {a = b} + {a <> b}, exists x : _, s = right _ x. +intros. +elim s. +intro. + absurd (a = a); auto. -Intro. -Split with b0; Reflexivity. +intro. +split with b0; reflexivity. -Save. +Qed. Module Type ELEM. Parameter T : Set. - Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}. + Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}. End ELEM. -Module Type SET[Elt : ELEM]. +Module Type SET (Elt: ELEM). Parameter T : Set. Parameter empty : T. Parameter add : Elt.T -> T -> T. @@ -40,56 +42,52 @@ Module Type SET[Elt : ELEM]. (* Axioms *) - Axiom find_empty_false : - (e:Elt.T) (find e empty) = false. + Axiom find_empty_false : forall e : Elt.T, find e empty = false. - Axiom find_add_true : - (s:T) (e:Elt.T) (find e (add e s)) = true. + Axiom find_add_true : forall (s : T) (e : Elt.T), find e (add e s) = true. - Axiom find_add_false : - (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> - (find e (add e' s))=(find e s). + Axiom + find_add_false : + forall (s : T) (e e' : Elt.T), e <> e' -> find e (add e' s) = find e s. End SET. -Module FuncDict[E : ELEM]. +Module FuncDict (E: ELEM). Definition T := E.T -> bool. - Definition empty := [e':E.T] false. - Definition find := [e':E.T] [s:T] (s e'). - Definition add := [e:E.T][s:T][e':E.T] - (ifte (E.eq_dec e e') true (find e' s)). + Definition empty (e' : E.T) := false. + Definition find (e' : E.T) (s : T) := s e'. + Definition add (e : E.T) (s : T) (e' : E.T) := + ifte (E.eq_dec e e') true (find e' s). - Lemma find_empty_false : (e:E.T) (find e empty) = false. - Auto. + Lemma find_empty_false : forall e : E.T, find e empty = false. + auto. Qed. - Lemma find_add_true : - (s:T) (e:E.T) (find e (add e s)) = true. + Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. - Intros. - Unfold find add. - Elim (Reflexivity_provable ? ? (E.eq_dec e e)). - Intros. - Rewrite H. - Auto. + intros. + unfold find, add in |- *. + elim (Reflexivity_provable _ _ (E.eq_dec e e)). + intros. + rewrite H. + auto. Qed. Lemma find_add_false : - (s:T) (e:E.T) (e':E.T) ~(e=e') -> - (find e (add e' s))=(find e s). - Intros. - Unfold add find. - Cut (EXT x:? | (E.eq_dec e' e)==(right ? ? x)). - Intros. - Elim H0. - Intros. - Rewrite H1. - Unfold ifte. - Reflexivity. - - Apply Disequality_provable. - Auto. + forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. + intros. + unfold add, find in |- *. + cut (exists x : _, E.eq_dec e' e = right _ x). + intros. + elim H0. + intros. + rewrite H1. + unfold ifte in |- *. + reflexivity. + + apply Disequality_provable. + auto. Qed. @@ -99,84 +97,81 @@ Module F : SET := FuncDict. Module Nat. - Definition T:=nat. - Lemma eq_dec : (a,a':T){a=a'}+{~ a=a'}. - Decide Equality. + Definition T := nat. + Lemma eq_dec : forall a a' : T, {a = a'} + {a <> a'}. + decide equality. Qed. End Nat. -Module SetNat:=F Nat. +Module SetNat := F Nat. -Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. -Apply SetNat.find_empty_false. -Save. +Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. +apply SetNat.find_empty_false. +Qed. (***************************************************************************) -Module Lemmas[G:SET][E:ELEM]. +Module Lemmas (G: SET) (E: ELEM). - Module ESet:=G E. + Module ESet := G E. - Lemma commute : (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 - (a:E.T)(ESet.find a S1)=(ESet.find a S2). + Lemma commute : + 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. - Intros. - Unfold S1 S2. - Elim (E.eq_dec a a1); Elim (E.eq_dec a a2); Intros H1 H2; - Try Rewrite <- H1; Try Rewrite <- H2; - Repeat - (Try (Rewrite ESet.find_add_true; Auto); - Try (Rewrite ESet.find_add_false; Auto); - Auto). - Save. + intros. + unfold S1, S2 in |- *. + elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2; + try rewrite <- H1; try rewrite <- H2; + repeat + (try ( rewrite ESet.find_add_true; auto); + try ( rewrite ESet.find_add_false; auto); auto). + Qed. End Lemmas. -Inductive list [A:Set] : Set := nil : (list A) - | cons : A -> (list A) -> (list A). +Inductive list (A : Set) : Set := + | nil : list A + | cons : A -> list A -> list A. -Module ListDict[E : ELEM]. - Definition T := (list E.T). +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] : bool := - Cases s of - nil => false - | (cons e' s') => (ifte (E.eq_dec e e') - true - (find e s')) - end. - - Definition find_empty_false := [e:elt] (refl_equal bool false). - - Lemma find_add_true : - (s:T) (e:E.T) (find e (add e s)) = true. - Intros. - Simpl. - Elim (Reflexivity_provable ? ? (E.eq_dec e e)). - Intros. - Rewrite H. - Auto. + Definition empty := nil elt. + Definition add (e : elt) (s : T) := cons elt e s. + Fixpoint find (e : elt) (s : T) {struct s} : bool := + match s with + | nil => false + | cons e' s' => ifte (E.eq_dec e e') true (find e s') + end. + + Definition find_empty_false (e : elt) := refl_equal false. + + Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. + intros. + simpl in |- *. + elim (Reflexivity_provable _ _ (E.eq_dec e e)). + intros. + rewrite H. + auto. Qed. Lemma find_add_false : - (s:T) (e:E.T) (e':E.T) ~(e=e') -> - (find e (add e' s))=(find e s). - Intros. - Simpl. - Elim (Disequality_provable ? ? ? H (E.eq_dec e e')). - Intros. - Rewrite H0. - Simpl. - Reflexivity. - Save. + forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. + intros. + simpl in |- *. + elim (Disequality_provable _ _ _ H (E.eq_dec e e')). + intros. + rewrite H0. + simpl in |- *. + reflexivity. + Qed. End ListDict. @@ -190,4 +185,3 @@ Module L : SET := ListDict. - diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v index 13c284181..8dadace77 100644 --- a/test-suite/modules/Tescik.v +++ b/test-suite/modules/Tescik.v @@ -1,30 +1,30 @@ Module Type ELEM. - Parameter A:Set. - Parameter x:A. + Parameter A : Set. + Parameter x : A. End ELEM. Module Nat. - Definition A:=nat. - Definition x:=O. + Definition A := nat. + Definition x := 0. End Nat. -Module List[X:ELEM]. - Inductive list : Set := nil : list - | cons : X.A -> list -> list. +Module List (X: ELEM). + Inductive list : Set := + | nil : list + | cons : X.A -> list -> list. - Definition head := - [l:list]Cases l of - nil => X.x - | (cons x _) => x - end. + Definition head (l : list) := match l with + | nil => X.x + | cons x _ => x + end. - Definition singl := [x:X.A] (cons x nil). + Definition singl (x : X.A) := cons x nil. - Lemma head_singl : (x:X.A)(head (singl x))=x. - Auto. + Lemma head_singl : forall x : X.A, head (singl x) = x. + auto. Qed. End List. -Module N:=(List Nat). +Module N := List Nat. \ No newline at end of file diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v index 0f8eef847..f4dc19b3e 100644 --- a/test-suite/modules/fun_objects.v +++ b/test-suite/modules/fun_objects.v @@ -1,32 +1,32 @@ -Implicit Arguments On. +Set Implicit Arguments. +Unset Strict Implicit. Module Type SIG. - Parameter id:(A:Set)A->A. + Parameter id : forall A : Set, A -> A. End SIG. -Module M[X:SIG]. - Definition idid := (X.id X.id). - Definition id := (idid X.id). +Module M (X: SIG). + Definition idid := X.id X.id. + Definition id := idid X.id. End M. -Module N:=M. +Module N := M. Module Nat. Definition T := nat. - Definition x := O. - Definition id := [A:Set][x:A]x. + Definition x := 0. + Definition id (A : Set) (x : A) := x. End Nat. -Module Z:=(N Nat). +Module Z := N Nat. -Check (Z.idid O). +Check (Z.idid 0). -Module P[Y:SIG] := N. +Module P (Y: SIG) := N. -Module Y:=P Nat Z. - -Check (Y.id O). +Module Y := P Nat Z. +Check (Y.id 0). diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v index fb734b5d5..9657c685d 100644 --- a/test-suite/modules/grammar.v +++ b/test-suite/modules/grammar.v @@ -1,15 +1,15 @@ Module N. -Definition f:=plus. -Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E]. -Check (f O O). +Definition f := plus. +(* : Syntax is discontinued *) +Check (f 0 0). End N. -Check (N.f O O). +Check (N.f 0 0). Import N. -Check (N.f O O). -Check (f O O). -Module M:=N. -Check (f O O). -Check (N.f O O). +Check (f 0 0). +Check (f 0 0). +Module M := N. +Check (f 0 0). +Check (f 0 0). Import M. -Check (f O O). -Check (N.f O O). +Check (f 0 0). +Check (N.f 0 0). \ No newline at end of file diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v index 94c344bbd..a4f9d3a28 100644 --- a/test-suite/modules/ind.v +++ b/test-suite/modules/ind.v @@ -1,13 +1,17 @@ Module Type SIG. - Inductive w:Set:=A:w. - Parameter f : w->w. + Inductive w : Set := + A : w. + Parameter f : w -> w. End SIG. -Module M:SIG. - Inductive w:Set:=A:w. - Definition f:=[x]Cases x of A => A end. +Module M : SIG. + Inductive w : Set := + A : w. + Definition f x := match x with + | A => A + end. End M. -Module N:=M. +Module N := M. -Check (N.f M.A). +Check (N.f M.A). \ No newline at end of file diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v index a9d22d79d..aad493cee 100644 --- a/test-suite/modules/mod_decl.v +++ b/test-suite/modules/mod_decl.v @@ -1,49 +1,49 @@ Module Type SIG. - Axiom A:Set. + Axiom A : Set. End SIG. Module M0. - Definition A:Set. - Exact nat. - Save. + Definition A : Set. + exact nat. + Qed. End M0. -Module M1:SIG. - Definition A:=nat. +Module M1 : SIG. + Definition A := nat. End M1. -Module M2<:SIG. - Definition A:=nat. +Module M2 <: SIG. + Definition A := nat. End M2. -Module M3:=M0. +Module M3 := M0. -Module M4:SIG:=M0. +Module M4 : SIG := M0. -Module M5<:SIG:=M0. +Module M5 <: SIG := M0. -Module F[X:SIG]:=X. +Module F (X: SIG) := X. Module Type T. Module M0. - Axiom A:Set. + Axiom A : Set. End M0. - Declare Module M1:SIG. + Declare Module M1: SIG. - Declare Module M2<:SIG. - Definition A:=nat. + Declare Module M2 <: SIG. + Definition A := nat. End M2. - Module M3:=M0. + Module M3 := M0. - Module M4:SIG:=M0. + Module M4 : SIG := M0. - Module M5<:SIG:=M0. + Module M5 <: SIG := M0. - Module M6:=F M0. + Module M6 := F M0. End T. diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v index 9e74a310d..45cf9f124 100644 --- a/test-suite/modules/modeq.v +++ b/test-suite/modules/modeq.v @@ -1,22 +1,22 @@ Module M. - Definition T:=nat. - Definition x:T:=O. + Definition T := nat. + Definition x : T := 0. End M. Module Type SIG. - Module M:=Top.M. + Module M := Top.M. Module Type SIG. - Parameter T:Set. + Parameter T : Set. End SIG. - Declare Module N:SIG. + Declare Module N: SIG. End SIG. Module Z. - Module M:=Top.M. + Module M := Top.M. Module Type SIG. - Parameter T:Set. + Parameter T : Set. End SIG. - Module N:=M. + Module N := M. End Z. -Module A:SIG:=Z. +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 58ae2a52d..9d24d6ce4 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -1,18 +1,17 @@ Module M. - Parameter rel:nat -> nat -> Prop. + Parameter rel : nat -> nat -> Prop. - Axiom w : (n:nat)(rel O (S n)). + Axiom w : forall n : nat, rel 0 (S n). - Hints Resolve w. + Hint Resolve w. - Grammar constr constr8 := - not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ]. + (* : Grammar is replaced by Notation *) Print Hint *. - Lemma w1 : (O#(S O)). - Auto. - Save. + Lemma w1 : rel 0 1. + auto. + Qed. End M. @@ -24,14 +23,13 @@ Auto. Import M. -Lemma w1 : (O#(S O)). -Auto. -Save. +Lemma w1 : rel 0 1. +auto. +Qed. -Check (O#O). +Check (rel 0 0). Locate rel. Locate Module M. -Module N:=Top.M. - +Module N := Top.M. diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v index 2231e0849..97337a125 100644 --- a/test-suite/modules/obj.v +++ b/test-suite/modules/obj.v @@ -1,16 +1,17 @@ -Implicit Arguments On. +Set Implicit Arguments. +Unset Strict Implicit. Module M. - Definition a:=[s:Set]s. + Definition a (s : Set) := s. Print a. End M. Print M.a. Module K. - Definition app:=[A,B:Set; f:(A->B); x:A](f x). + Definition app (A B : Set) (f : A -> B) (x : A) := f x. Module N. - Definition apap:=[A,B:Set](app (app 1!A 2!B)). + Definition apap (A B : Set) := app (app (A:=A) (B:=B)). Print app. Print apap. End N. @@ -20,7 +21,6 @@ End K. Print K.app. Print K.N.apap. -Module W:=K.N. +Module W := K.N. Print W.apap. - diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v index 418ece442..070f859ea 100644 --- a/test-suite/modules/objects.v +++ b/test-suite/modules/objects.v @@ -1,33 +1,33 @@ Module Type SET. - Axiom T:Set. - Axiom x:T. + Axiom T : Set. + Axiom x : T. End SET. -Implicit Arguments On. +Set Implicit Arguments. +Unset Strict Implicit. -Module M[X:SET]. +Module M (X: SET). Definition T := nat. - Definition x := O. - Definition f := [A:Set][x:A]X.x. + Definition x := 0. + Definition f (A : Set) (x : A) := X.x. End M. -Module N:=M. +Module N := M. Module Nat. Definition T := nat. - Definition x := O. + Definition x := 0. End Nat. -Module Z:=(N Nat). +Module Z := N Nat. -Check (Z.f O). +Check (Z.f 0). -Module P[Y:SET] := N. +Module P (Y: SET) := N. -Module Y:=P Z Nat. - -Check (Y.f O). +Module Y := P Z Nat. +Check (Y.f 0). diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v index 6061ace34..f806a7c41 100644 --- a/test-suite/modules/pliczek.v +++ b/test-suite/modules/pliczek.v @@ -1,3 +1,3 @@ Require Export plik. -Definition tutu := [X:Set](toto X). +Definition tutu (X : Set) := toto X. \ No newline at end of file diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v index f1f59df0f..50bfd9604 100644 --- a/test-suite/modules/plik.v +++ b/test-suite/modules/plik.v @@ -1,4 +1,3 @@ -Definition toto:=[x:Set]x. +Definition toto (x : Set) := x. -Grammar constr constr8 := - toto [ "#" constr7($b) ] -> [ (toto $b) ]. +(* : Grammar is replaced by Notation *) \ No newline at end of file diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v index c09a74324..4cb6291df 100644 --- a/test-suite/modules/sig.v +++ b/test-suite/modules/sig.v @@ -1,29 +1,29 @@ Module M. Module Type SIG. - Parameter T:Set. - Parameter x:T. + Parameter T : Set. + Parameter x : T. End SIG. - Module N:SIG. - Definition T:=nat. - Definition x:=O. + Module N : SIG. + Definition T := nat. + Definition x := 0. End N. End M. -Module N:=M. +Module N := M. Module Type SPRYT. Module N. - Definition T:=M.N.T. - Parameter x:T. + Definition T := M.N.T. + Parameter x : T. 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. - Parameter x:T. + Definition T : Set := M.N.T. + Parameter x : T. End SIG. -Module J:SIG:=M.N. +Module J : SIG := M.N. \ No newline at end of file diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v index 1bd4faef0..5eec07758 100644 --- a/test-suite/modules/sub_objects.v +++ b/test-suite/modules/sub_objects.v @@ -1,33 +1,32 @@ Set Implicit Arguments. +Unset Strict Implicit. Module M. - Definition id:=[A:Set][x:A]x. + Definition id (A : Set) (x : A) := x. Module Type SIG. - Parameter idid:(A:Set)A->A. + Parameter idid : forall A : Set, A -> A. End SIG. Module N. - Definition idid:=[A:Set][x:A](id x). - Grammar constr constr8 := - not_eq [ "#" constr7($b) ] -> [ (idid $b) ]. - Notation inc := (plus (S O)). + Definition idid (A : Set) (x : A) := id x. + (* : Grammar is replaced by Notation *) + Notation inc := (plus 1). End N. - Definition zero:=(N.idid O). + Definition zero := N.idid 0. End M. -Definition zero := (M.N.idid O). -Definition jeden := (M.N.inc O). +Definition zero := M.N.idid 0. +Definition jeden := M.N.inc 0. -Module Goly:=M.N. +Module Goly := M.N. -Definition Gole_zero := (Goly.idid O). -Definition Goly_jeden := (Goly.inc O). +Definition Gole_zero := Goly.idid 0. +Definition Goly_jeden := Goly.inc 0. Module Ubrany : M.SIG := M.N. -Definition Ubrane_zero := (Ubrany.idid O). - +Definition Ubrane_zero := Ubrany.idid 0. -- cgit v1.2.3