From a40e92559339d41eb3a757968de4367d77df712f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 3 Oct 2009 15:55:11 +0000
Subject: Fixed small name freshness bug in Functional Scheme ("Heq" name was
 not refreshed late enough).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12369 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/functional_principles_proofs.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 90eb499422..949150ba54 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -562,14 +562,14 @@ let heq_id = id_of_string "Heq"
 
 let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
   fun g ->
-    let heq_id = pf_get_new_id heq_id g in
     let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
     tclTHENLIST
       [
 	(* We first introduce the variables *)
 	tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
 	(* Then the equation itself *)
-	introduction_no_check heq_id;
+	intro_using heq_id;
+	onLastHypId (fun heq_id -> tclTHENLIST [
 	(* Then the new hypothesis *)
 	tclMAP introduction_no_check dyn_infos.rec_hyps;
 	(* observe_tac "after_introduction"  *)(fun g' ->
@@ -599,7 +599,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	   }
 	 in
 	 clean_goal_with_heq ptes_infos continue_tac new_infos  g'
-      )
+      )])
     ]
       g
 
-- 
cgit v1.2.3