diff options
| author | Hugo Herbelin | 2016-03-28 17:53:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-03-28 18:28:58 +0200 |
| commit | d670c6b6ceab80f1c3b6b74ffb53579670c0e621 (patch) | |
| tree | 38b375155df8cd81638ebcab7401d35ec8f08502 | |
| parent | 044d9f62bf0e1140268a3236e4bb53f10d716078 (diff) | |
Fixing an incorrect use of prod_appvect on a term which was not a
product in setoid_rewrite.
Before commit e8c47b652, it was raising an error which has been turned
to an anomaly.
This impacted Compcert where the former error was (apparently) caught
so that setoid_rewrite was returning back to ordinary rewrite.
| -rw-r--r-- | ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/setoid_test.v | 8 |
2 files changed, 9 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 20d4651efa..cf2a01052f 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1046,7 +1046,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | x -> x in let res = - { rew_car = prod_appvect r.rew_car args; + { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args; rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args); rew_prf = prf; rew_evars = r.rew_evars } in 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. |