diff options
| -rw-r--r-- | test-suite/success/Cases.v | 71 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v | 22 | ||||
| -rw-r--r-- | test-suite/success/Mod_params.v | 84 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 6 | ||||
| -rw-r--r-- | test-suite/success/RecTutorial.v | 69 | ||||
| -rw-r--r-- | test-suite/success/Reset.v | 7 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 3 | ||||
| -rw-r--r-- | test-suite/success/hyps_inclusion.v | 8 |
8 files changed, 129 insertions, 141 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 745529bf6..f445ca8ea 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -100,7 +100,7 @@ Type (fun x : nat => match x return nat with | x => x end). -Section testlist. +Module Type testlist. Parameter A : Set. Inductive list : Set := | nil : list @@ -119,7 +119,6 @@ Definition titi (a : A) (l : list) := | nil => l | cons b l => l end. -Reset list. End testlist. @@ -913,71 +912,77 @@ Type | LeS n m _ => (S n, S m) end). - +Module Type F_v1. Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := match h in (Le n m) return (Le n (S m)) with | LeO m' => LeO (S m') | LeS n' m' h' => LeS n' (S m') (F n' m' h') end. +End F_v1. -Reset F. - +Module Type F_v2. Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := match h in (Le n m) return (Le n (S m)) with | LeS n m h => LeS n (S m) (F n m h) | LeO m => LeO (S m) end. +End F_v2. (* Rend la longueur de la liste *) -Definition length1 (n : nat) (l : listn n) := + +Module Type L1. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => 1 | _ => 0 end. +End L1. -Reset length1. -Definition length1 (n : nat) (l : listn n) := +Module Type L1'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => 1 | _ => 0 end. +End L1'. - -Definition length2 (n : nat) (l : listn n) := +Module Type L2. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => S n | _ => 0 end. +End L2. -Reset length2. - -Definition length2 (n : nat) (l : listn n) := +Module Type L2'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => S n | _ => 0 end. +End L2'. -Definition length3 (n : nat) (l : listn n) := +Module Type L3. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ l) => S n | consn n _ _ => 1 | _ => 0 end. +End L3. - -Reset length3. - -Definition length3 (n : nat) (l : listn n) := +Module Type L3'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ l) => S n | consn n _ _ => 1 | _ => 0 end. - +End L3'. Type match LeO 0 return nat with | LeS n m h => n + m @@ -1256,7 +1261,7 @@ Type match (0, 0) with | (x, y) => (S x, S y) end. - +Module Type test_concat. Parameter concat : forall A : Set, List A -> List A -> List A. @@ -1273,6 +1278,7 @@ Type | _, _ => Nil nat end. +End test_concat. Inductive redexes : Set := | VAR : nat -> redexes @@ -1295,7 +1301,6 @@ Type (fun n : nat => match n with | _ => 0 end). -Reset concat. Parameter concat : forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m). @@ -1383,6 +1388,7 @@ Type (* I.e. to test manipulation of elimination predicate *) (* ===================================================================== *) +Module Type test_term. Parameter LTERM : nat -> Set. Inductive TERM : Type := @@ -1397,7 +1403,8 @@ Type | oper op1 l1, oper op2 l2 => False | _, _ => False end. -Reset LTERM. + +End test_term. @@ -1493,6 +1500,7 @@ Type end. +Module Type ff. Parameter ff : forall n m : nat, n <> m -> S n <> S m. Parameter discr_r : forall n : nat, 0 <> S n. @@ -1505,6 +1513,7 @@ Type | S x => or_intror (S x = 0) (discr_l x) end). +Module Type eqdec. Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := match n, m return (n = m \/ n <> m) with @@ -1518,7 +1527,9 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := end end. -Reset eqdec. +End eqdec. + +Module Type eqdec'. Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := match n return (forall m : nat, n = m \/ n <> m) with @@ -1540,6 +1551,7 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := end end. +End eqdec'. Inductive empty : forall n : nat, listn n -> Prop := intro_empty : empty 0 niln. @@ -1554,7 +1566,10 @@ Type | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y) end). -Reset ff. +End ff. + +Module Type ff'. + Parameter ff : forall n m : nat, n <> m -> S n <> S m. Parameter discr_r : forall n : nat, 0 <> S n. Parameter discr_l : forall n : nat, S n <> 0. @@ -1566,6 +1581,7 @@ Type | S x => or_intror (S x = 0) (discr_l x) end). +Module Type eqdec. Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := match n, m return (n = m \/ n <> m) with @@ -1578,7 +1594,10 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := | or_intror h => or_intror (S x = S y) (ff x y h) end end. -Reset eqdec. + +End eqdec. + +Module Type eqdec'. Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := match n return (forall m : nat, n = m \/ n <> m) with @@ -1600,6 +1619,8 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := end end. +End eqdec'. +End ff'. (* ================================================== *) (* Pour tester parametres *) diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index d3b7cf3f3..bfead53c0 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -222,7 +222,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci. de l'arite de chaque operateur *) -Section Sig. +Module Sig. Record Signature : Type := {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}. @@ -277,7 +277,7 @@ Type | _, _ => False end. - +Module Type Version1. Definition equalT (t1 t2 : TERM) : Prop := match t1, t2 with @@ -294,12 +294,15 @@ Definition EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) | _, _ => False end. +End Version1. + -Reset equalT. (* ------------------------------------------------------------------*) (* Initial exemple (without patterns) *) (*-------------------------------------------------------------------*) +Module Version2. + Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 return (TERM -> Prop) with | var v1 => @@ -347,11 +350,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version2. (* ---------------------------------------------------------------- *) (* Version with simple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version3. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -388,8 +393,9 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version3. -Reset equalT. +Module Version4. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -423,10 +429,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version4. + (* ---------------------------------------------------------------- *) (* Version with multiple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version5. Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := match t1, t2 with @@ -445,6 +454,7 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := | _, _ => False end. +End Version5. (* ------------------------------------------------------------------ *) diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v index 74228bbbf..515161660 100644 --- a/test-suite/success/Mod_params.v +++ b/test-suite/success/Mod_params.v @@ -20,59 +20,31 @@ End Q. #trace Nametab.exists_cci;; *) -Module M. -Reset M. -Module M (X: SIG). -Reset M. -Module M (X Y: SIG). -Reset M. -Module M (X: SIG) (Y: SIG). -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG). -Reset M. -Module M (X: SIG) (Y: 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. -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG) : SIG. -Reset M. -Module M (X: SIG) (Y: SIG) : SIG. -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. +Module M01. End M01. +Module M02 (X: SIG). End M02. +Module M03 (X Y: SIG). End M03. +Module M04 (X: SIG) (Y: SIG). End M04. +Module M05 (X Y: SIG) (Z1 Z: SIG). End M05. +Module M06 (X: SIG) (Y: SIG). End M06. +Module M07 (X Y: SIG) (Z1 Z: SIG). End M07. +Module M08 : SIG. End M08. +Module M09 (X: SIG) : SIG. End M09. +Module M10 (X Y: SIG) : SIG. End M10. +Module M11 (X: SIG) (Y: SIG) : SIG. End M11. +Module M12 (X Y: SIG) (Z1 Z: SIG) : SIG. End M12. +Module M13 (X: SIG) (Y: SIG) : SIG. End M13. +Module M14 (X Y: SIG) (Z1 Z: SIG) : SIG. End M14. +Module M15 := F Q. +Module M16 (X: FSIG) := X Q. +Module M17 (X Y: FSIG) := X Q. +Module M18 (X: FSIG) (Y: SIG) := X Y. +Module M19 (X Y: FSIG) (Z1 Z: SIG) := X Z. +Module M20 (X: FSIG) (Y: SIG) := X Y. +Module M21 (X Y: FSIG) (Z1 Z: SIG) := X Z. +Module M22 : SIG := F Q. +Module M23 (X: FSIG) : SIG := X Q. +Module M24 (X Y: FSIG) : SIG := X Q. +Module M25 (X: FSIG) (Y: SIG) : SIG := X Y. +Module M26 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. +Module M27 (X: FSIG) (Y: SIG) : SIG := X Y. +Module M28 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 3c34ff928..89f110593 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -17,10 +17,12 @@ Check (nat |= nat --> nat). (* Check that first non empty definition at an empty level can be of any associativity *) -Definition marker := O. +Module Type v1. Notation "x +1" := (S x) (at level 8, left associativity). -Reset marker. +End v1. +Module Type v2. Notation "x +1" := (S x) (at level 8, right associativity). +End v2. (* Check that empty levels (here 8 and 2 in pattern) are added in the right order *) diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 2602c7e35..64048fe24 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -1,3 +1,5 @@ +Module Type LocalNat. + Inductive nat : Set := | O : nat | S : nat->nat. @@ -5,7 +7,8 @@ Check nat. Check O. Check S. -Reset nat. +End LocalNat. + Print nat. @@ -477,10 +480,10 @@ Qed. -(* -Check (fun (P:Prop->Prop)(p: ex_Prop P) => +Fail Check (fun (P:Prop->Prop)(p: ex_Prop P) => match p with exP_intro X HX => X end). +(* Error: Incorrect elimination of "p" in the inductive type "ex_Prop", the return type has sort "Type" while it should be @@ -489,12 +492,11 @@ Incorrect elimination of "p" in the inductive type Elimination of an inductive object of sort "Prop" is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs - *) -(* -Check (match prop_inject with (prop_intro P p) => P end). +Fail Check (match prop_inject with (prop_intro p) => p end). +(* Error: Incorrect elimination of "prop_inject" in the inductive type "prop", the return type has sort "Type" while it should be @@ -503,13 +505,12 @@ Incorrect elimination of "prop_inject" in the inductive type Elimination of an inductive object of sort "Prop" is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs - *) Print prop_inject. (* prop_inject = -prop_inject = prop_intro prop (fun H : prop => H) +prop_inject = prop_intro prop : prop *) @@ -520,26 +521,24 @@ Inductive typ : Type := Definition typ_inject: typ. split. exact typ. +Fail Defined. (* -Defined. - Error: Universe Inconsistency. *) Abort. -(* -Inductive aSet : Set := +Fail Inductive aSet : Set := aSet_intro: Set -> aSet. - - +(* User error: Large non-propositional inductive types must be in Type - *) Inductive ex_Set (P : Set -> Prop) : Type := exS_intro : forall X : Set, P X -> ex_Set P. +Module Type Version1. + Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop := c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p). @@ -553,21 +552,15 @@ Goal ~(comes_from_the_left _ _ (or_intror True I)). *) Abort. -Reset comes_from_the_left. - -(* +End Version1. - - - - - - Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop := +Fail Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop := match H with | or_introl p => True | or_intror q => False end. +(* Error: Incorrect elimination of "H" in the inductive type "or", the return type has sort "Type" while it should be @@ -576,7 +569,6 @@ Incorrect elimination of "H" in the inductive type Elimination of an inductive object of sort "Prop" is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs - *) Definition comes_from_the_left_sumbool @@ -737,6 +729,7 @@ Fixpoint plus'' (n p:nat) {struct n} : nat := | S m => plus'' m (S p) end. +Module Type even_test_v1. Fixpoint even_test (n:nat) : bool := match n @@ -745,8 +738,9 @@ Fixpoint even_test (n:nat) : bool := | S (S p) => even_test p end. +End even_test_v1. -Reset even_test. +Module even_test_v2. Fixpoint even_test (n:nat) : bool := match n @@ -761,12 +755,8 @@ with odd_test (n:nat) : bool := | S p => even_test p end. - - Eval simpl in even_test. - - Eval simpl in (fun x : nat => even_test x). Eval simpl in (fun x : nat => plus 5 x). @@ -774,6 +764,8 @@ Eval simpl in (fun x : nat => even_test (plus 5 x)). Eval simpl in (fun x : nat => even_test (plus x 5)). +End even_test_v2. + Section Principle_of_Induction. Variable P : nat -> Prop. @@ -866,14 +858,13 @@ Print Acc. Require Import Minus. -(* -Fixpoint div (x y:nat){struct x}: nat := +Fail Fixpoint div (x y:nat){struct x}: nat := if eq_nat_dec x 0 then 0 else if eq_nat_dec y 0 then x else S (div (x-y) y). - +(* Error: Recursive definition of div is ill-formed. In environment @@ -971,19 +962,15 @@ Proof. intros A v;inversion v. Abort. -(* - Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), - n= 0 -> v = Vnil A. -Toplevel input, characters 40281-40287 -> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vnil A. -> ^^^^^^ +Fail Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), + n= 0 -> v = Vector.nil A. +(* Error: In environment A : Set n : nat v : Vector.t A n -e : n = 0 -The term "Vnil A" has type "Vector.t A 0" while it is expected to have type +The term "[]" has type "Vector.t A 0" while it is expected to have type "Vector.t A n" *) Require Import JMeq. diff --git a/test-suite/success/Reset.v b/test-suite/success/Reset.v deleted file mode 100644 index b71ea69d7..000000000 --- a/test-suite/success/Reset.v +++ /dev/null @@ -1,7 +0,0 @@ -(* Check Reset Section *) - -Section A. -Definition B := Prop. -End A. - -Reset A. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 8e829e061..d3c761019 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -97,13 +97,14 @@ Qed. (* Check use of unification of bindings types in specialize *) +Module Type Test. Variable P : nat -> Prop. Variable L : forall (l : nat), P l -> P l. Goal P 0 -> True. intros. specialize L with (1:=H). Abort. -Reset P. +End Test. (* Two examples that show that hnf_constr is used when unifying types of bindings (a simplification of a script from Field_Theory) *) diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v index af81e53d6..ebd90a40e 100644 --- a/test-suite/success/hyps_inclusion.v +++ b/test-suite/success/hyps_inclusion.v @@ -19,14 +19,16 @@ red in H. (* next tactic was failing wrt bug #1325 because type-checking the goal detected a syntactically different type for the section variable H *) case 0. -Reset A. +Abort. +End A. (* Variant with polymorphic inductive types for bug #1325 *) -Section A. +Section B. Variable H:not True. Inductive I (n:nat) : Type := C : H=H -> I n. Goal I 0. red in H. case 0. -Reset A. +Abort. +End B. |