summaryrefslogtreecommitdiff
path: root/test-suite/failure/universes-buraliforti.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /test-suite/failure/universes-buraliforti.v
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/failure/universes-buraliforti.v')
-rw-r--r--test-suite/failure/universes-buraliforti.v20
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index 1f96ab34..7b62a0c5 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -37,7 +37,7 @@ Section Inverse_Image.
Qed.
Lemma WF_inverse_image : WF B R -> WF A Rof.
- red in |- *; intros; apply ACC_inverse_image; auto.
+ red; intros; apply ACC_inverse_image; auto.
Qed.
End Inverse_Image.
@@ -90,7 +90,7 @@ 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.
+red; auto.
Defined.
@@ -108,7 +108,7 @@ apply sym_eq; assumption.
intros.
apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
Defined.
(* The embedding relation is well founded *)
@@ -144,7 +144,7 @@ Section Subsets.
exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
exact WF_emb.
-red in |- *; trivial.
+red; trivial.
exact emb_wit.
Defined.
@@ -160,7 +160,7 @@ End Subsets.
- the upper bound is a, which is in F(b) since a < b
*)
Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
exists
(sub x)
(Rof _ _ emb (witness x))
@@ -171,10 +171,10 @@ exists
apply WF_inverse_image.
exact WF_emb.
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
trivial.
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
apply emb_wit.
Defined.
@@ -222,10 +222,10 @@ 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 |- *.
+ end.
+case H; simpl.
exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
Defined.
(* The following command raises 'Error: Universe Inconsistency'.