diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/setoid_test.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 0465c4b3fb..4c173a3cd5 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -166,3 +166,11 @@ 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 at 1. change (beq_nat x 0 = foo_neg y). Abort. +(* This should not raise an anomaly as it did for some time in early 2016 *) + +Definition t := nat -> bool. +Definition h (a b : t) := forall n, a n = b n. +Goal forall a b, h a b -> a 0 = true. +intros. +rewrite H. (* Fallback on ordinary rewrite without anomaly *) +Abort. |