diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
| commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /test-suite/failure/universes-buraliforti.v | |
| parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
| parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) | |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/failure/universes-buraliforti.v')
| -rw-r--r-- | test-suite/failure/universes-buraliforti.v | 20 |
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'. |