From 8b660087beb2209e52bc4412dc82c6727963c6a5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Nov 2016 20:26:15 +0100
Subject: Elim API using EConstr.

---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 plugins/funind/recdef.ml                       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 503cafdd50..940f1669ab 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1626,7 +1626,7 @@ let prove_principle_for_gen
 	[
 	  Proofview.V82.of_tactic (generalize [lemma]);
 	  Proofview.V82.of_tactic (Simple.intro hid);
-	  Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
+	  Proofview.V82.of_tactic (Elim.h_decompose_and (EConstr.mkVar hid));
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
 	     tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d5ee42af8d..74affa3964 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1314,7 +1314,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	       (fun g ->
 		  let ids = pf_ids_of_hyps g in
 		  tclTHEN
-		    (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
+		    (Proofview.V82.of_tactic (Elim.h_decompose_and (EConstr.mkVar hid)))
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
 		       lid := List.rev (List.subtract Id.equal ids' ids);
-- 
cgit v1.2.3