diff options
Diffstat (limited to 'test-suite/failure')
38 files changed, 498 insertions, 0 deletions
diff --git a/test-suite/failure/Case1.v b/test-suite/failure/Case1.v new file mode 100644 index 00000000..fafcafc1 --- /dev/null +++ b/test-suite/failure/Case1.v @@ -0,0 +1 @@ +Type Cases O of x => O | O => (S O) end. diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v new file mode 100644 index 00000000..ee47544d --- /dev/null +++ b/test-suite/failure/Case10.v @@ -0,0 +1 @@ +Type [x:nat]<nat> Cases x of ((S x) as b) => (S b) end. diff --git a/test-suite/failure/Case11.v b/test-suite/failure/Case11.v new file mode 100644 index 00000000..c39a76ca --- /dev/null +++ b/test-suite/failure/Case11.v @@ -0,0 +1 @@ +Type [x:nat]<nat> Cases x of ((S x) as b) => (S b x) end. diff --git a/test-suite/failure/Case12.v b/test-suite/failure/Case12.v new file mode 100644 index 00000000..b56eac0d --- /dev/null +++ b/test-suite/failure/Case12.v @@ -0,0 +1,7 @@ + +Type [x:nat]<nat> Cases x of + ((S x) as b) => <nat>Cases x of + x => x + end + end. + diff --git a/test-suite/failure/Case13.v b/test-suite/failure/Case13.v new file mode 100644 index 00000000..8a4d75b6 --- /dev/null +++ b/test-suite/failure/Case13.v @@ -0,0 +1,5 @@ +Type [x:nat]<nat> Cases x of + ((S x) as b) => <nat>Cases x of + x => (S b x) + end + end. diff --git a/test-suite/failure/Case14.v b/test-suite/failure/Case14.v new file mode 100644 index 00000000..a198d068 --- /dev/null +++ b/test-suite/failure/Case14.v @@ -0,0 +1,8 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Definition NIL := (Nil nat). +Type <(List nat)>Cases (Nil nat) of + NIL => NIL + | _ => NIL + end. diff --git a/test-suite/failure/Case15.v b/test-suite/failure/Case15.v new file mode 100644 index 00000000..a27b07f8 --- /dev/null +++ b/test-suite/failure/Case15.v @@ -0,0 +1,6 @@ +(* Non exhaustive pattern-matching *) + +Check [x]Cases x x of + O (S (S y)) => true + | O (S x) => false + | (S y) O => true end.
\ No newline at end of file diff --git a/test-suite/failure/Case16.v b/test-suite/failure/Case16.v new file mode 100644 index 00000000..f994a8f2 --- /dev/null +++ b/test-suite/failure/Case16.v @@ -0,0 +1,9 @@ +(* Check for redundant clauses *) + +Check [x]Cases x x of + O (S (S y)) => true + | (S _) (S (S y)) => true + | _ (S (S x)) => false + | (S y) O => true + | _ _ => true +end. diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v new file mode 100644 index 00000000..183f612b --- /dev/null +++ b/test-suite/failure/Case2.v @@ -0,0 +1,13 @@ +Inductive IFExpr : Set := + Var : nat -> IFExpr + | Tr : IFExpr + | Fa : IFExpr + | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. + +Type [F:IFExpr] + <Prop>Cases F of + (IfE (Var _) H I) => True + | (IfE _ _ _) => False + | _ => True + end. + diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v new file mode 100644 index 00000000..2c651b87 --- /dev/null +++ b/test-suite/failure/Case3.v @@ -0,0 +1,7 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Type [l:(List nat)]<nat>Cases l of + (Nil nat) =>O + | (Cons a l) => (S a) + end. diff --git a/test-suite/failure/Case4.v b/test-suite/failure/Case4.v new file mode 100644 index 00000000..d00c9a05 --- /dev/null +++ b/test-suite/failure/Case4.v @@ -0,0 +1,7 @@ + +Definition Berry := [x,y,z:bool] + Cases x y z of + true false _ => O + | false _ true => (S O) + | _ true false => (S (S O)) +end. diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v new file mode 100644 index 00000000..bdb5544b --- /dev/null +++ b/test-suite/failure/Case5.v @@ -0,0 +1,3 @@ +Inductive MS: Set := X:MS->MS | Y:MS->MS. + +Type [p:MS]<nat>Cases p of (X x) => O end. diff --git a/test-suite/failure/Case6.v b/test-suite/failure/Case6.v new file mode 100644 index 00000000..f588d275 --- /dev/null +++ b/test-suite/failure/Case6.v @@ -0,0 +1,10 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + + +Type <(List nat)>Cases (Nil nat) of + NIL => NIL + | (CONS _ _) => NIL + + end. + diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v new file mode 100644 index 00000000..3718f198 --- /dev/null +++ b/test-suite/failure/Case7.v @@ -0,0 +1,22 @@ +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Definition length1:= [n:nat] [l:(listn n)] + Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S O) + | _ => O + end. + +Type [n:nat] + [l:(listn n)] + <nat>Cases n of + O => O + | (S n) => + <([_:nat]nat)>Cases l of + niln => (S O) + | l' => (length1 (S n) l') + end + end. + diff --git a/test-suite/failure/Case8.v b/test-suite/failure/Case8.v new file mode 100644 index 00000000..7f6bb615 --- /dev/null +++ b/test-suite/failure/Case8.v @@ -0,0 +1,8 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Type <nat>Cases (Nil nat) of + ((Nil_) as b) =>b + |((Cons _ _ _) as d) => d + end. + diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v new file mode 100644 index 00000000..e8d8e89a --- /dev/null +++ b/test-suite/failure/Case9.v @@ -0,0 +1,6 @@ +Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. +Type <nat>Cases (compare O O) of + (* k<i *) (left _ _ (left _ _ _)) => O + | (* k=i *) (left _ _ _) => O + | (* k>i *) (right _ _ _) => O end. + diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v new file mode 100644 index 00000000..ca8e3c68 --- /dev/null +++ b/test-suite/failure/ClearBody.v @@ -0,0 +1,8 @@ +(* ClearBody must check that removing the body of definition does not + invalidate the well-typabilility of the visible goal *) + +Goal True. +LetTac n:=O. +LetTac I:=(refl_equal nat O). +Change (n=O) in (Type of I). +ClearBody n. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v new file mode 100644 index 00000000..fb9a27bb --- /dev/null +++ b/test-suite/failure/Tauto.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(**** Tactics Tauto and Intuition ****) + +(**** Tauto: + Tactic for automating proof in Intuionnistic Propositional Calculus, based on + the contraction-free LJT of Dickhoff ****) + +(**** Intuition: + Simplifications of goals, based on LJT calcul ****) + +(* Fails because Tauto does not perform any Apply *) +Goal ((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y). +Proof. + Tauto. diff --git a/test-suite/failure/cases.v b/test-suite/failure/cases.v new file mode 100644 index 00000000..a27b07f8 --- /dev/null +++ b/test-suite/failure/cases.v @@ -0,0 +1,6 @@ +(* Non exhaustive pattern-matching *) + +Check [x]Cases x x of + O (S (S y)) => true + | O (S x) => false + | (S y) O => true end.
\ No newline at end of file diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v new file mode 100644 index 00000000..0bf7091c --- /dev/null +++ b/test-suite/failure/check.v @@ -0,0 +1,3 @@ +Implicits eq [1]. + +Check (eq bool true). diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v new file mode 100644 index 00000000..56cd73f4 --- /dev/null +++ b/test-suite/failure/clash_cons.v @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Teste la verification d'unicite des noms de constr *) + + +Inductive X : Set := + cons : X. + +Inductive Y : Set := + cons : Y. + diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v new file mode 100644 index 00000000..fcfd29fe --- /dev/null +++ b/test-suite/failure/clashes.v @@ -0,0 +1,8 @@ +(* Submitted by David Nowak *) + +(* Simpler to forbid the definition of n as a global than to write it + S.n to keep n accessible... *) + +Section S. +Variable n:nat. +Inductive P : Set := n : P. diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v new file mode 100644 index 00000000..2ac6c4f0 --- /dev/null +++ b/test-suite/failure/coqbugs0266.v @@ -0,0 +1,7 @@ +(* It is forbidden to erase a variable (or a local def) that is used in + the current goal. *) +Section S. +Local a:=O. +Definition b:=a. +Goal b=b. +Clear a. diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v new file mode 100644 index 00000000..742e9774 --- /dev/null +++ b/test-suite/failure/fixpoint1.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Fixpoint PreParadox [u:unit] : False := (PreParadox u). +Definition Paradox := (PreParadox tt).
\ No newline at end of file diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v new file mode 100644 index 00000000..aff43ff1 --- /dev/null +++ b/test-suite/failure/illtype1.v @@ -0,0 +1,8 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Check (S S). diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v new file mode 100644 index 00000000..d0256619 --- /dev/null +++ b/test-suite/failure/ltac1.v @@ -0,0 +1,5 @@ +(* Check all variables are different in a Context *) +Tactic Definition X := Match Context With [ x:?; x:? |- ? ] -> Apply x. +Goal True->True->True. +Intros. +X. diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v new file mode 100644 index 00000000..55925a7a --- /dev/null +++ b/test-suite/failure/ltac2.v @@ -0,0 +1,6 @@ +(* Check that Match arguments are forbidden *) +Tactic Definition E x := Apply x. +Goal True->True. +E (Match Context With [ |- ? ] -> Intro H). +(* Should fail with "Immediate Match producing tactics not allowed in + local definitions" *) diff --git a/test-suite/failure/ltac3.v b/test-suite/failure/ltac3.v new file mode 100644 index 00000000..bfccc546 --- /dev/null +++ b/test-suite/failure/ltac3.v @@ -0,0 +1,2 @@ +(* Proposed by Benjamin *) +Definition A := Try REflexivity. diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v new file mode 100644 index 00000000..d1e4e892 --- /dev/null +++ b/test-suite/failure/ltac4.v @@ -0,0 +1,4 @@ +(* Check static globalisation of tactic names *) +(* Proposed by Benjamin (mars 2002) *) +Goal (n:nat)n=n. +Induction n; Try REflexivity. diff --git a/test-suite/failure/params_ind.v b/test-suite/failure/params_ind.v new file mode 100644 index 00000000..20689128 --- /dev/null +++ b/test-suite/failure/params_ind.v @@ -0,0 +1,4 @@ +Inductive list [A:Set] : Set := + nil : (list A) +| cons : A -> (list A->A)-> (list A). + diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v new file mode 100644 index 00000000..b43eb899 --- /dev/null +++ b/test-suite/failure/positivity.v @@ -0,0 +1,8 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Inductive t:Set := c: (t -> nat) -> t. diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v new file mode 100644 index 00000000..8f3aedac --- /dev/null +++ b/test-suite/failure/redef.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Definition toto := Set. +Definition toto := Set. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v new file mode 100644 index 00000000..e8ca8494 --- /dev/null +++ b/test-suite/failure/search.v @@ -0,0 +1,8 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +SearchPattern ? = ? outside n_existe_pas. diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v new file mode 100644 index 00000000..01d46133 --- /dev/null +++ b/test-suite/failure/universes-buraliforti.v @@ -0,0 +1,227 @@ +(* Check that Burali-Forti paradox does not go through *) + +(* Source: contrib/Rocq/PARADOX/{Logics,BuraliForti},v *) + +(* Some properties about relations on objects in Type *) + + Inductive ACC [A : Type; R : A->A->Prop] : A->Prop := + ACC_intro : (x:A)((y:A)(R y x)->(ACC A R y))->(ACC A R x). + + Lemma ACC_nonreflexive: + (A:Type)(R:A->A->Prop)(x:A)(ACC A R x)->(R x x)->False. +Induction 1; Intros. +Exact (H1 x0 H2 H2). +Save. + + Definition WF := [A:Type][R:A->A->Prop](x:A)(ACC A R x). + + +Section Inverse_Image. + + Variables A,B:Type; R:B->B->Prop; f:A->B. + + Definition Rof : A->A->Prop := [x,y:A](R (f x) (f y)). + + Remark ACC_lemma : (y:B)(ACC B R y)->(x:A)(y==(f x))->(ACC A Rof x). + Induction 1; Intros. + Constructor; Intros. + Apply (H1 (f y0)); Trivial. + Elim H2 using eqT_ind_r; Trivial. + Save. + + Lemma ACC_inverse_image : (x:A)(ACC B R (f x)) -> (ACC A Rof x). + Intros; Apply (ACC_lemma (f x)); Trivial. + Save. + + Lemma WF_inverse_image: (WF B R)->(WF A Rof). + Red; Intros; Apply ACC_inverse_image; Auto. + Save. + +End Inverse_Image. + + +(* Remark: the paradox is written in Type, but also works in Prop or Set. *) + +Section Burali_Forti_Paradox. + + Definition morphism := [A:Type][R:A->A->Prop][B:Type][S:B->B->Prop][f:A->B] + (x,y:A)(R x y)->(S (f x) (f y)). + + (* The hypothesis of the paradox: + assumes there exists an universal system of notations, i.e: + - A type A0 + - An injection i0 from relations on any type into A0 + - The proof that i0 is injective modulo morphism + *) + Variable A0 : Type. (* Type_i *) + Variable i0 : (X:Type)(X->X->Prop)->A0. (* X: Type_j *) + Hypothesis inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) + (i0 X1 R1)==(i0 X2 R2) + ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). + + (* Embedding of x in y: x and y are images of 2 well founded relations + R1 and R2, the ordinal of R2 being strictly greater than that of R1. + *) + Record emb [x,y:A0]: Prop := { + X1: Type; + R1: X1->X1->Prop; + eqx: x==(i0 X1 R1); + X2: Type; + R2: X2->X2->Prop; + eqy: y==(i0 X2 R2); + W2: (WF X2 R2); + f: X1->X2; + fmorph: (morphism X1 R1 X2 R2 f); + maj: X2; + majf: (z:X1)(R2 (f z) maj) }. + + + Lemma emb_trans: (x,y,z:A0)(emb x y)->(emb y z)->(emb x z). +Intros. +Case H; Intros. +Case H0; Intros. +Generalize eqx0; Clear eqx0. +Elim eqy using eqT_ind_r; Intro. +Case (inj ? ? ? ? eqx0); Intros. +Exists X1 R1 X3 R3 [x:X1](f0 (x0 (f x))) maj0; Trivial. +Red; Auto. +Defined. + + + Lemma ACC_emb: (X:Type)(R:X->X->Prop)(x:X)(ACC X R x) + ->(Y:Type)(S:Y->Y->Prop)(f:Y->X)(morphism Y S X R f) + ->((y:Y)(R (f y) x)) + ->(ACC A0 emb (i0 Y S)). +Induction 1; Intros. +Constructor; Intros. +Case H4; Intros. +Elim eqx using eqT_ind_r. +Case (inj X2 R2 Y S). +Apply sym_eqT; Assumption. + +Intros. +Apply H1 with y:=(f (x1 maj)) f:=[x:X1](f (x1 (f0 x))); Try Red; Auto. +Defined. + + (* The embedding relation is well founded *) + Lemma WF_emb: (WF A0 emb). +Constructor; Intros. +Case H; Intros. +Elim eqx using eqT_ind_r. +Apply ACC_emb with X:=X2 R:=R2 x:=maj f:=f; Trivial. +Defined. + + + (* The following definition enforces Type_j >= Type_i *) + Definition Omega: A0 := (i0 A0 emb). + + +Section Subsets. + + Variable a: A0. + + (* We define the type of elements of A0 smaller than a w.r.t embedding. + The Record is in Type, but it is possible to avoid such structure. *) + Record sub: Type := { + witness : A0; + emb_wit : (emb witness a) }. + + (* F is its image through i0 *) + Definition F : A0 := (i0 sub (Rof ? ? emb witness)). + + (* F is embedded in Omega: + - the witness projection is a morphism + - a is an upper bound because emb_wit proves that witness is + smaller than a. + *) + Lemma F_emb_Omega: (emb F Omega). +Exists sub (Rof ? ? emb witness) A0 emb witness a; Trivial. +Exact WF_emb. + +Red; Trivial. + +Exact emb_wit. +Defined. + +End Subsets. + + + Definition fsub: (a,b:A0)(emb a b)->(sub a)->(sub b):= + [_,_][H][x] + (Build_sub ? (witness ? x) (emb_trans ? ? ? (emb_wit ? x) H)). + + (* F is a morphism: a < b => F(a) < F(b) + - the morphism from F(a) to F(b) is fsub above + - the upper bound is a, which is in F(b) since a < b + *) + Lemma F_morphism: (morphism A0 emb A0 emb F). +Red; Intros. +Exists (sub x) (Rof ? ? emb (witness x)) (sub y) + (Rof ? ? emb (witness y)) (fsub x y H) (Build_sub ? x H); +Trivial. +Apply WF_inverse_image. +Exact WF_emb. + +Unfold morphism Rof fsub; Simpl; Intros. +Trivial. + +Unfold Rof fsub; Simpl; Intros. +Apply emb_wit. +Defined. + + + (* Omega is embedded in itself: + - F is a morphism + - Omega is an upper bound of the image of F + *) + Lemma Omega_refl: (emb Omega Omega). +Exists A0 emb A0 emb F Omega; Trivial. +Exact WF_emb. + +Exact F_morphism. + +Exact F_emb_Omega. +Defined. + + (* The paradox is that Omega cannot be embedded in itself, since + the embedding relation is well founded. + *) + Theorem Burali_Forti: False. +Apply ACC_nonreflexive with A0 emb Omega. +Apply WF_emb. + +Exact Omega_refl. + +Defined. + +End Burali_Forti_Paradox. + + + (* The following type seems to satisfy the hypothesis of the paradox. + But it does not! + *) + Record A0: Type := (* Type_i' *) + i0 { X0: Type; R0: X0->X0->Prop }. (* X0: Type_j' *) + + + (* Note: this proof uses a large elimination of A0. *) + Lemma inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) + (i0 X1 R1)==(i0 X2 R2) + ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). +Intros. +Change Cases (i0 X1 R1) (i0 X2 R2) of + (i0 x1 r1) (i0 x2 r2) => (EXT f | (morphism x1 r1 x2 r2 f)) + end. +Case H; Simpl. +Exists [x:X1]x. +Red; Trivial. +Defined. + +(* The following command raises 'Error: Universe Inconsistency'. + To allow large elimination of A0, i0 must not be a large constructor. + Hence, the constraint Type_j' < Type_i' is added, which is incompatible + with the constraint j >= i in the paradox. +*) + + Definition Paradox: False := (Burali_Forti A0 i0 inj). + diff --git a/test-suite/failure/universes-sections1.v b/test-suite/failure/universes-sections1.v new file mode 100644 index 00000000..c4eef34b --- /dev/null +++ b/test-suite/failure/universes-sections1.v @@ -0,0 +1,8 @@ +(* Check that constraints on definitions are preserved by discharging *) + +Section A. + Definition Type2 := Type. + Definition Type1 := Type : Type2. +End A. + +Definition Inconsistency := Type2 : Type1. diff --git a/test-suite/failure/universes-sections2.v b/test-suite/failure/universes-sections2.v new file mode 100644 index 00000000..1872dac1 --- /dev/null +++ b/test-suite/failure/universes-sections2.v @@ -0,0 +1,10 @@ +(* Check that constraints on locals are preserved by discharging *) + +Definition Type2 := Type. + +Section A. + Local Type1 := Type : Type2. + Definition Type1' := Type1. +End A. + +Definition Inconsistency := Type2 : Type1'. diff --git a/test-suite/failure/universes.v b/test-suite/failure/universes.v new file mode 100644 index 00000000..6fada6f1 --- /dev/null +++ b/test-suite/failure/universes.v @@ -0,0 +1,3 @@ +Definition Type2 := Type. +Definition Type1 := Type : Type2. +Definition Inconsistency := Type2 : Type1. diff --git a/test-suite/failure/universes2.v b/test-suite/failure/universes2.v new file mode 100644 index 00000000..a6c8ba43 --- /dev/null +++ b/test-suite/failure/universes2.v @@ -0,0 +1,5 @@ +(* Example submitted by Randy Pollack *) + +Parameter K: (T:Type)T->T. +Check (K ((T:Type)T->T) K). +(* Universe Inconsistency *) |