From b77579ac873975a15978c5a4ecf312d577746d26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 21:59:18 +0100
Subject: Tacred API using EConstr.

---
 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 12ed758ba9..bdbf0242d7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -692,7 +692,7 @@ let mkDestructEq :
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
-          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
+          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], EConstr.of_constr expr] in
           redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2))
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
-- 
cgit v1.2.3