diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-07 14:14:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-07 14:54:34 +0200 |
| commit | 9d50e5426cc816789650b7f541793a9ba773d14c (patch) | |
| tree | 929bf2346c2d3c35200f9d1722d5957f71698617 /test-suite/success/setoid_test.v | |
| parent | 17c2147fe0a73b4e0af6481afd73df5cdcf8aefd (diff) | |
An example which failed in 8.5 and that d670c6b6 fixes.
Thanks to Matthieu for the example.
Diffstat (limited to 'test-suite/success/setoid_test.v')
| -rw-r--r-- | test-suite/success/setoid_test.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 4c173a3cd..1f24ef2a6 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -170,7 +170,12 @@ Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y) 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. + +Instance subrelh : subrelation h (Morphisms.pointwise_relation nat eq). +Proof. intros x y H; assumption. Qed. + +Goal forall a b, h a b -> a 0 = b 0. intros. -rewrite H. (* Fallback on ordinary rewrite without anomaly *) -Abort. +setoid_rewrite H. (* Fallback on ordinary rewrite without anomaly *) +reflexivity. +Qed. |