From 802f5513983080884971b3d9c7ed0cc3ee76c404 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 25 Sep 2018 12:58:57 +0200
Subject: Fixes #8553 (regression of tactic "change" under binders).

---
 plugins/funind/recdef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7298342e1e..633d98a585 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -713,7 +713,7 @@ let mkDestructEq :
     observe_tclTHENLIST (str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
-        let changefun patvars sigma =
+        let changefun patvars env sigma =
           pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
         in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
-- 
cgit v1.2.3