summaryrefslogtreecommitdiff
path: root/test-suite/failure
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/failure
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/failure')
-rw-r--r--test-suite/failure/Case1.v1
-rw-r--r--test-suite/failure/Case10.v1
-rw-r--r--test-suite/failure/Case11.v1
-rw-r--r--test-suite/failure/Case12.v7
-rw-r--r--test-suite/failure/Case13.v5
-rw-r--r--test-suite/failure/Case14.v8
-rw-r--r--test-suite/failure/Case15.v6
-rw-r--r--test-suite/failure/Case16.v9
-rw-r--r--test-suite/failure/Case2.v13
-rw-r--r--test-suite/failure/Case3.v7
-rw-r--r--test-suite/failure/Case4.v7
-rw-r--r--test-suite/failure/Case5.v3
-rw-r--r--test-suite/failure/Case6.v10
-rw-r--r--test-suite/failure/Case7.v22
-rw-r--r--test-suite/failure/Case8.v8
-rw-r--r--test-suite/failure/Case9.v6
-rw-r--r--test-suite/failure/ClearBody.v8
-rw-r--r--test-suite/failure/Tauto.v20
-rw-r--r--test-suite/failure/cases.v6
-rw-r--r--test-suite/failure/check.v3
-rw-r--r--test-suite/failure/clash_cons.v16
-rw-r--r--test-suite/failure/clashes.v8
-rw-r--r--test-suite/failure/coqbugs0266.v7
-rw-r--r--test-suite/failure/fixpoint1.v9
-rw-r--r--test-suite/failure/illtype1.v8
-rw-r--r--test-suite/failure/ltac1.v5
-rw-r--r--test-suite/failure/ltac2.v6
-rw-r--r--test-suite/failure/ltac3.v2
-rw-r--r--test-suite/failure/ltac4.v4
-rw-r--r--test-suite/failure/params_ind.v4
-rw-r--r--test-suite/failure/positivity.v8
-rw-r--r--test-suite/failure/redef.v9
-rw-r--r--test-suite/failure/search.v8
-rw-r--r--test-suite/failure/universes-buraliforti.v227
-rw-r--r--test-suite/failure/universes-sections1.v8
-rw-r--r--test-suite/failure/universes-sections2.v10
-rw-r--r--test-suite/failure/universes.v3
-rw-r--r--test-suite/failure/universes2.v5
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 *)