diff options
| author | Hugo Herbelin | 2018-09-26 11:41:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-26 11:41:05 +0200 |
| commit | bebd946584b33a5e263393bd88e8571cd5fa5af2 (patch) | |
| tree | 514fd72bd77f76b1d4e11783160c606a776330e3 | |
| parent | ccb701d78394a108daf25e62d40ba059aa3fce62 (diff) | |
Fix for Coq PR#8554 (term builder for tactic "change" takes an environment).
| -rw-r--r-- | src/tac2tactics.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index 3c464469f0..25431af2ea 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -159,8 +159,7 @@ let specialize c pat = let change pat c cl = let open Tac2ffi in Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let c subst sigma = + let c subst env sigma = let subst = Array.map_of_list snd (Id.Map.bindings subst) in delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma in |