From bebd946584b33a5e263393bd88e8571cd5fa5af2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Sep 2018 11:41:05 +0200
Subject: Fix for Coq PR#8554 (term builder for tactic "change" takes an
 environment).

---
 src/tac2tactics.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3