From b7d58843654963754593b0c9e44c0a5b7b7af16e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 28 May 2018 17:02:46 +0200
Subject: Tactics.introduction: remove dangerous option ~check

In locally nameless mode (proof mode) names in the context *must*
be distinct otherwise the term representation makes no sense.
---
 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 83fe1fc2f9..5336948642 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -598,7 +598,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 (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
+        tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps;
 	observe_tac "after_introduction" (fun g' ->
 	   (* We get infos on the equations introduced*)
 	   let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
-- 
cgit v1.2.3