From c32728e7bf0ba0449b60ea49df7f92fb6b70923d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Nov 2014 00:56:29 +0100
Subject: Removing the legacy intro tactic code.

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

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8e6bbcefdd..d7344d3558 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -589,7 +589,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	Proofview.V82.of_tactic (intro_using heq_id);
 	onLastHypId (fun heq_id -> tclTHENLIST [
 	(* Then the new hypothesis *)
-	tclMAP introduction_no_check dyn_infos.rec_hyps;
+	tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
 	observe_tac "after_introduction" (fun g' ->
 	   (* We get infos on the equations introduced*)
 	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
-- 
cgit v1.2.3