Fix for Coq PR#8554 (term builder for tactic "change" takes an enviro…

…nment).
coq · Oct 23, 2018 · a69551a · a69551a
1 parent 2c1a089
commit a69551a
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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