1 files changed, 130 insertions, 120 deletions

diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index 01d46133..d18d2119 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -4,38 +4,41 @@
 
 (* 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).
+  Inductive ACC (A : Type) (R : A -> A -> Prop) : A -> Prop :=
+      ACC_intro :
+        forall x : A, (forall 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.
+  Lemma ACC_nonreflexive :
+   forall (A : Type) (R : A -> A -> Prop) (x : A),
+   ACC A R x -> R x x -> False.
+simple induction 1; intros.
+exact (H1 x0 H2 H2).
+Qed.
 
-  Definition WF := [A:Type][R:A->A->Prop](x:A)(ACC A R x).
+  Definition WF (A : Type) (R : A -> A -> Prop) := forall x : A, ACC A R x.
 
 
 Section Inverse_Image.
 
-  Variables A,B:Type; R:B->B->Prop; f:A->B.
+  Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B).
 
-  Definition Rof : A->A->Prop := [x,y:A](R (f x) (f y)).
+  Definition Rof (x y : A) : Prop := 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.
+  Remark ACC_lemma :
+   forall y : B, ACC B R y -> forall x : A, y = f x -> ACC A Rof x.
+    simple induction 1; intros.
+    constructor; intros.
+    apply (H1 (f y0)); trivial.
+    elim H2 using eq_ind_r; trivial.
+    Qed.
 
-  Lemma ACC_inverse_image : (x:A)(ACC B R (f x)) -> (ACC A Rof x).
-    Intros; Apply (ACC_lemma (f x)); Trivial.
-    Save.
+  Lemma ACC_inverse_image : forall x : A, ACC B R (f x) -> ACC A Rof x.
+    intros; apply (ACC_lemma (f x)); trivial.
+    Qed.
 
-  Lemma WF_inverse_image: (WF B R)->(WF A Rof).
-    Red; Intros; Apply ACC_inverse_image; Auto.
-    Save.
+  Lemma WF_inverse_image : WF B R -> WF A Rof.
+    red in |- *; intros; apply ACC_inverse_image; auto.
+    Qed.
 
 End Inverse_Image.
 
@@ -44,8 +47,9 @@ End Inverse_Image.
 
 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)).
+  Definition morphism (A : Type) (R : A -> A -> Prop) 
+    (B : Type) (S : B -> B -> Prop) (f : A -> B) :=
+    forall 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:
@@ -53,120 +57,125 @@ Section Burali_Forti_Paradox.
       - 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)).
+  Variable A0 : Type.                     (* Type_i *)
+  Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
+  Hypothesis
+    inj :
+      forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
+        (R2 : X2 -> X2 -> Prop),
+      i0 X1 R1 = i0 X2 R2 -> exists 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.
+  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 : forall z : X1, R2 (f z) maj}.
+
+
+  Lemma emb_trans : forall 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 eq_ind_r; intro.
+case (inj _ _ _ _ eqx0); intros.
+exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
+red in |- *; 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.
+  Lemma ACC_emb :
+   forall (X : Type) (R : X -> X -> Prop) (x : X),
+   ACC X R x ->
+   forall (Y : Type) (S : Y -> Y -> Prop) (f : Y -> X),
+   morphism Y S X R f -> (forall y : Y, R (f y) x) -> ACC A0 emb (i0 Y S).
+simple induction 1; intros.
+constructor; intros.
+case H4; intros.
+elim eqx using eq_ind_r.
+case (inj X2 R2 Y S).
+apply sym_eq; assumption.
+
+intros.
+apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
+ try red in |- *; 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.
+  Lemma WF_emb : WF A0 emb.
+constructor; intros.
+case H; intros.
+elim eqx using eq_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).
+  Definition Omega : A0 := i0 A0 emb.
 
 
 Section Subsets.
 
-  Variable a: A0.
+  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) }.
+  Record sub : Type :=  {witness : A0; emb_wit : emb witness a}.
 
   (* F is its image through i0 *)
-  Definition F : A0 := (i0 sub (Rof ? ? emb witness)).
+  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.
+  Lemma F_emb_Omega : emb F Omega.
+exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
+exact WF_emb.
 
-Red; Trivial.
+red in |- *; trivial.
 
-Exact emb_wit.
+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)).
+  Definition fsub (a b : A0) (H : emb a b) (x : sub a) : 
+    sub b := 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.
+  Lemma F_morphism : morphism A0 emb A0 emb F.
+red in |- *; 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 in |- *; simpl in |- *; intros.
+trivial.
+
+unfold Rof, fsub in |- *; simpl in |- *; intros.
+apply emb_wit.
 Defined.
 
 
@@ -174,23 +183,23 @@ Defined.
      - 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.
+  Lemma Omega_refl : emb Omega Omega.
+exists A0 emb A0 emb F Omega; trivial.
+exact WF_emb.
 
-Exact F_morphism.
+exact F_morphism.
 
-Exact F_emb_Omega.
+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.
+  Theorem Burali_Forti : False.
+apply ACC_nonreflexive with A0 emb Omega.
+apply WF_emb.
 
-Exact Omega_refl.
+exact Omega_refl.
 
 Defined.
 
@@ -200,21 +209,23 @@ 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' *)
+  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.
+  Lemma inj :
+   forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
+     (R2 : X2 -> X2 -> Prop),
+   i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
+intros.
+change
+  match i0 X1 R1, i0 X2 R2 with
+  | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
+  end in |- *.
+case H; simpl in |- *.
+exists (fun x : X1 => x).
+red in |- *; trivial.
 Defined.
 
 (* The following command raises 'Error: Universe Inconsistency'.
@@ -223,5 +234,4 @@ Defined.
    with the constraint j >= i in the paradox.
 *)
 
-  Definition Paradox: False := (Burali_Forti A0 i0 inj).
-
+  Definition Paradox : False := Burali_Forti A0 i0 inj.