diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-07 14:58:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-07 16:57:34 +0200 |
| commit | 83608720aac2a0a464649aca8b2a23ce395679ae (patch) | |
| tree | a1f72f80743b29c18a52c8281ac976d5d1cfba43 | |
| parent | f6a8ce665815af9609163198f609e1db8ca49b47 (diff) | |
Fixing an incorrect use of prod_appvect on a term which was not a
product in setoid_rewrite.
Backport of d670c6b6ce from trunk.
| -rw-r--r-- | tactics/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 803e187ff..21abafbf1 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1028,7 +1028,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 |