diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/typeclasses/clrewrite.v | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/typeclasses/clrewrite.v')
| -rw-r--r-- | test-suite/typeclasses/clrewrite.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/typeclasses/clrewrite.v b/test-suite/typeclasses/clrewrite.v index 2978fda2..f21acd4c 100644 --- a/test-suite/typeclasses/clrewrite.v +++ b/test-suite/typeclasses/clrewrite.v @@ -15,7 +15,7 @@ Section Equiv. Qed. Tactic Notation "simpl" "*" := auto || relation_tac. - + Goal eqA x y -> eqA y x /\ True. intros H ; clrewrite H. split ; simpl*. @@ -27,13 +27,13 @@ Section Equiv. Qed. Goal eqA x y -> eqA y z -> eqA x y. - intros H. + intros H. clrewrite H. intro. refl. Qed. - + Goal eqA x y -> eqA z y -> eqA x y. - intros H. + intros H. clrewrite <- H at 2. clrewrite <- H at 1. intro. refl. @@ -54,7 +54,7 @@ Section Equiv. clrewrite <- H. refl. Qed. - + Goal eqA x y -> True /\ True /\ False /\ eqA x x -> True /\ True /\ False /\ eqA x y. Proof. intros. @@ -70,12 +70,12 @@ Section Trans. Variables x y z w : A. Tactic Notation "simpl" "*" := auto || relation_tac. - + (* Typeclasses eauto := debug. *) Goal R x y -> R y x -> R y y -> R x x. Proof with auto. - intros H H' H''. + intros H H' H''. clrewrite <- H' at 2. clrewrite H at 1... @@ -86,11 +86,11 @@ Section Trans. clrewrite H. refl. Qed. - + Goal R x y -> R z y -> R x y. - intros H. + intros H. clrewrite <- H at 2. - intro. + intro. clrewrite H at 1. Abort. |