aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2tactics.ml3
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