diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-21 17:08:00 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-21 17:08:00 +0000 |
commit | 440af48253bb8b9870c78e1392f0c7a10c23feee (patch) | |
tree | ab74f752c9b6e2084b4fad018926ca7094e9ff2c | |
parent | 18c1f91426baea8fdce67a1a6b41a1ab106f93ee (diff) |
Fix test-suite script.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13846 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | test-suite/success/setoid_test.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index d5096ea65..63ca8aff4 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -144,15 +144,14 @@ Section mult. Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). Proof. intros. setoid_rewrite fold_lemma. - change (fold A A (λ x0 : A, ab A x0) x = anat A (fold A nat (ab nat) x)). + change (fold A A (fun x0 : A, ab A x0) x = anat A (fold A nat (ab nat) x)). Abort. End mult. -(** Current semantics for rewriting with typeclass constraints in the lemma - fixes the instance at the first unification. Using @ to make them metavariables - allow different instances to be used. [at] can be used to select the instance - too. *) +(** Current semantics for rewriting with typeclass constraints in the lemma + does not fix the instance at the first unification, use [at], or simply rewrite for + this semantics. *) Require Import Arith. @@ -161,8 +160,8 @@ Instance: Foo nat. admit. Defined. Instance: Foo bool. admit. Defined. Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. -Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = foo_neg y). Abort. +Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort. Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. -Proof. intros. setoid_rewrite <- @foo_prf. change (beq_nat x 0 = y). Abort. +Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort. |