From a3848b0a10064fb7e206a503ac8b829cb9ce4666 Mon Sep 17 00:00:00 2001 From: coq Date: Tue, 13 Aug 2002 14:44:24 +0000 Subject: Petites corrections ici et la git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/modules/Nametab.v | 110 ++++++++++++++++++++++++--------------- test-suite/modules/Przyklad.v | 32 ++++++------ test-suite/modules/fun_objects.v | 20 +++---- test-suite/modules/grammar.v | 10 ++-- test-suite/modules/modul.v | 8 +-- test-suite/modules/modulik.v | 5 -- test-suite/modules/obj.v | 14 ++--- test-suite/modules/objects.v | 20 +++---- test-suite/modules/sub_objects.v | 16 +++--- 9 files changed, 129 insertions(+), 106 deletions(-) delete mode 100644 test-suite/modules/modulik.v (limited to 'test-suite/modules') diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v index 9d8c49ef7..9773bc6f4 100644 --- a/test-suite/modules/Nametab.v +++ b/test-suite/modules/Nametab.v @@ -1,35 +1,35 @@ -Module M. - Definition id:=[x:Set]x. - Module M. - Definition zero:(id nat):= O. - Definition id:=Set. - Definition nacik:id:=nat. - End M. -End M. - -Module M. +Module Q. Module N. Module K. Definition id:=Set. End K. End N. -End M. - +End Q. Locate id. Locate K.id. Locate N.K.id. -Locate M.N.K.id. -Locate Top.M.N.K.id. +Locate Q.N.K.id. +Locate Top.Q.N.K.id. Locate K. Locate N.K. -Locate M.N.K. -Locate Scratch.M.N.K. +Locate Q.N.K. +Locate Top.Q.N.K. Locate N. -Locate M.N. -Locate Scratch.M.N. -Locate M. -Locate Scratch.M. +Locate Q.N. +Locate Top.Q.N. +Locate Q. +Locate Top.Q. + + +Module Type SIG. +End SIG. + +Module Type FSIG[X:SIG]. +End FSIG. + +Module F[X:SIG]. +End F. (* #trace Nametab.push;; @@ -40,46 +40,74 @@ Locate Scratch.M. *) Module M. +Reset M. Module M[X:SIG]. +Reset M. Module M[X,Y:SIG]. +Reset M. Module M[X:SIG;Y:SIG]. -Module M[X,Y:SIG;X,Z:SIG]. +Reset M. +Module M[X,Y:SIG;Z1,Z:SIG]. +Reset M. Module M[X:SIG][Y:SIG]. -Module M[X,Y:SIG][X,Z:SIG]. +Reset M. +Module M[X,Y:SIG][Z1,Z:SIG]. +Reset M. Module M:SIG. +Reset M. Module M[X:SIG]:SIG. +Reset M. Module M[X,Y:SIG]:SIG. +Reset M. Module M[X:SIG;Y:SIG]:SIG. -Module M[X,Y:SIG;X,Z:SIG]:SIG. +Reset M. +Module M[X,Y:SIG;Z1,Z:SIG]:SIG. +Reset M. Module M[X:SIG][Y:SIG]:SIG. -Module M[X,Y:SIG][X,Z:SIG]:SIG. -Module M:=(M N). -Module M[X:SIG]:=(M N). -Module M[X,Y:SIG]:=(M N). -Module M[X:SIG;Y:SIG]:=(M N). -Module M[X,Y:SIG;X,Z:SIG]:=(M N). -Module M[X:SIG][Y:SIG]:=(M N). -Module M[X,Y:SIG][X,Z:SIG]:=(M N). -Module M:SIG:=(M N). -Module M[X:SIG]:SIG:=(M N). -Module M[X,Y:SIG]:SIG:=(M N). -Module M[X:SIG;Y:SIG]:SIG:=(M N). -Module M[X,Y:SIG;X,Z:SIG]:SIG:=(M N). -Module M[X:SIG][Y:SIG]:SIG:=(M N). -Module M[X,Y:SIG][X,Z:SIG]:SIG:=(M N). +Reset M. +Module M[X,Y:SIG][Z1,Z:SIG]:SIG. +Reset M. +Module M:=(F Q). +Reset M. +Module M[X:FSIG]:=(X Q). +Reset M. +Module M[X,Y:FSIG]:=(X Q). +Reset M. +Module M[X:FSIG;Y:SIG]:=(X Y). +Reset M. +Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z). +Reset M. +Module M[X:FSIG][Y:SIG]:=(X Y). +Reset M. +Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z). +Reset M. +Module M:SIG:=(F Q). +Reset M. +Module M[X:FSIG]:SIG:=(X Q). +Reset M. +Module M[X,Y:FSIG]:SIG:=(X Q). +Reset M. +Module M[X:FSIG;Y:SIG]:SIG:=(X Y). +Reset M. +Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z). +Reset M. +Module M[X:FSIG][Y:SIG]:SIG:=(X Y). +Reset M. +Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z). +Reset M. -Moduletype SIG. +Module Type ELEM. Parameter A:Set. Parameter x:A. -EndT SIG. +End ELEM. Module Nat. Definition A:=nat. Definition x:=O. End Nat. -Module List[X:SIG]. +Module List[X:ELEM]. Inductive list : Set := nil : list | cons : X.A -> list -> list. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index ecf9a8c25..4f4c2066d 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -27,12 +27,12 @@ Split with b0; Reflexivity. Save. -Modtype ELEM. +Module Type ELEM. Parameter T : Set. Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}. -EndT ELEM. +End ELEM. -Modtype SET[Elt : ELEM]. +Module Type SET[Elt : ELEM]. Parameter T : Set. Parameter empty : T. Parameter add : Elt.T -> T -> T. @@ -50,9 +50,9 @@ Modtype SET[Elt : ELEM]. (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> (find e (add e' s))=(find e s). -EndT SET. +End SET. -Mod 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'). @@ -93,20 +93,20 @@ Mod FuncDict[E : ELEM]. Qed. -EndM FuncDict. +End FuncDict. -Mod F : SET := FuncDict. +Module F : SET := FuncDict. -Mod Nat. +Module Nat. Definition T:=nat. Lemma eq_dec : (a,a':T){a=a'}+{~ a=a'}. Decide Equality. Qed. -EndM Nat. +End Nat. -Mod SetNat:=F Nat. +Module SetNat:=F Nat. Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. @@ -114,9 +114,9 @@ Apply SetNat.find_empty_false. Save. (***************************************************************************) -Mod Lemmas[G:SET][E:ELEM]. +Module Lemmas[G:SET][E:ELEM]. - Mod 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 @@ -132,13 +132,13 @@ Mod Lemmas[G:SET][E:ELEM]. Try (Rewrite ESet.find_add_false; Auto); Auto). Save. -EndM Lemmas. +End Lemmas. Inductive list [A:Set] : Set := nil : (list A) | cons : A -> (list A) -> (list A). -Mod ListDict[E : ELEM]. +Module ListDict[E : ELEM]. Definition T := (list E.T). Definition elt := E.T. @@ -179,10 +179,10 @@ Mod ListDict[E : ELEM]. Save. -EndM ListDict. +End ListDict. -Mod L : SET := ListDict. +Module L : SET := ListDict. diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v index b14c3f793..0f8eef847 100644 --- a/test-suite/modules/fun_objects.v +++ b/test-suite/modules/fun_objects.v @@ -1,29 +1,29 @@ Implicit Arguments On. -Modtype SIG. +Module Type SIG. Parameter id:(A:Set)A->A. -EndT SIG. +End SIG. -Mod M[X:SIG]. +Module M[X:SIG]. Definition idid := (X.id X.id). Definition id := (idid X.id). -EndM M. +End M. -Mod N:=M. +Module N:=M. -Mod Nat. +Module Nat. Definition T := nat. Definition x := O. Definition id := [A:Set][x:A]x. -EndM Nat. +End Nat. -Mod Z:=(N Nat). +Module Z:=(N Nat). Check (Z.idid O). -Mod P[Y:SIG] := N. +Module P[Y:SIG] := N. -Mod Y:=P Nat Z. +Module Y:=P Nat Z. Check (Y.id O). diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v index 7751e9f38..fb734b5d5 100644 --- a/test-suite/modules/grammar.v +++ b/test-suite/modules/grammar.v @@ -1,15 +1,15 @@ -Mod N. +Module N. Definition f:=plus. Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E]. Check (f O O). -EndM N. +End N. Check (N.f O O). -Imp N. +Import N. Check (N.f O O). Check (f O O). -Mod M:=N. +Module M:=N. Check (f O O). Check (N.f O O). -Imp M. +Import M. Check (f O O). Check (N.f O O). diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v index ba333c525..5612ea755 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -1,4 +1,4 @@ -Mod M. +Module M. Parameter rel:nat -> nat -> Prop. Axiom w : (n:nat)(rel O (S n)). @@ -14,13 +14,13 @@ Mod M. Auto. Save. -EndM M. +End M. (*Lemma w1 : (M.rel O (S O)). Auto. *) -Imp M. +Import M. Print Hint *. Lemma w1 : (O#(S O)). @@ -35,5 +35,5 @@ Locate rel. Locate M. -Mod N:=Scratch.M. +Module N:=Top.M. diff --git a/test-suite/modules/modulik.v b/test-suite/modules/modulik.v deleted file mode 100644 index 50d985e52..000000000 --- a/test-suite/modules/modulik.v +++ /dev/null @@ -1,5 +0,0 @@ -Definition toto := Set. - -Mod M. - Definition id:=[X:Set]X. -EndM M. diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v index b02bdf189..2231e0849 100644 --- a/test-suite/modules/obj.v +++ b/test-suite/modules/obj.v @@ -1,26 +1,26 @@ Implicit Arguments On. -Mod M. +Module M. Definition a:=[s:Set]s. Print a. -EndM M. +End M. Print M.a. -Mod K. +Module K. Definition app:=[A,B:Set; f:(A->B); x:A](f x). - Mod N. + Module N. Definition apap:=[A,B:Set](app (app 1!A 2!B)). Print app. Print apap. - EndM N. + End N. Print N.apap. -EndM K. +End K. Print K.app. Print K.N.apap. -Mod 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 8183c67c6..c2d1c52dd 100644 --- a/test-suite/modules/objects.v +++ b/test-suite/modules/objects.v @@ -1,32 +1,32 @@ Reset Initial. -Modtype SET. +Module Type SET. Axiom T:Set. Axiom x:T. -EndT SET. +End SET. Implicit Arguments On. -Mod M[X:SET]. +Module M[X:SET]. Definition T := nat. Definition x := O. Definition f := [A:Set][x:A]X.x. -EndM M. +End M. -Mod N:=M. +Module N:=M. -Mod Nat. +Module Nat. Definition T := nat. Definition x := O. -EndM Nat. +End Nat. -Mod Z:=(N Nat). +Module Z:=(N Nat). Check (Z.f O). -Mod P[Y:SET] := N. +Module P[Y:SET] := N. -Mod Y:=P Z Nat. +Module Y:=P Z Nat. Check (Y.f O). diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v index f800dec52..73fd6f322 100644 --- a/test-suite/modules/sub_objects.v +++ b/test-suite/modules/sub_objects.v @@ -3,33 +3,33 @@ Reset Initial. Set Implicit Arguments. -Mod M. +Module M. Definition id:=[A:Set][x:A]x. - Modtype SIG. + Module Type SIG. Parameter idid:(A:Set)A->A. - EndT SIG. + End SIG. - Mod N. + Module N. Definition idid:=[A:Set][x:A](id x). Grammar constr constr8 := not_eq [ "#" constr7($b) ] -> [ (idid $b) ]. Syntactic Definition inc := (plus (S O)). - EndM N. + End N. Definition zero:=(N.idid O). -EndM M. +End M. Definition zero := (M.N.idid O). Definition jeden := (M.N.inc O). -Mod Goly:=M.N. +Module Goly:=M.N. Definition Gole_zero := (Goly.idid O). Definition Goly_jeden := (Goly.inc O). -Mod Ubrany : M.SIG := M.N. +Module Ubrany : M.SIG := M.N. Definition Ubrane_zero := (Ubrany.idid O). -- cgit v1.2.3