diff options
Diffstat (limited to 'test-suite/failure/subtyping2.v')
-rw-r--r-- | test-suite/failure/subtyping2.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v index addd3b45..48fc2fff 100644 --- a/test-suite/failure/subtyping2.v +++ b/test-suite/failure/subtyping2.v @@ -54,7 +54,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. @@ -104,7 +104,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. @@ -122,7 +122,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 *) @@ -158,7 +158,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. @@ -174,7 +174,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)) @@ -185,10 +185,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. @@ -230,10 +230,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'. |