Imported Upstream version 8.0pl1upstream/8.0pl1

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 *)