From 505df17983e546305278c6332e5976d751c01b9b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Oct 2003 08:53:20 +0000
Subject: Correction bug FreshId

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4683 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index da5ab1772d..d57309a616 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1059,7 +1059,7 @@ let eval_opt_ident ist = option_app (eval_ident ist)
 
 (* Interpretation of constructions *)
 
-(* Extracted the constr list from lfun *)
+(* Extract the constr list from lfun *)
 let rec constr_list_aux env = function
   | (id,v)::tl -> 
       let (l1,l2) = constr_list_aux env tl in
@@ -1070,6 +1070,12 @@ let rec constr_list_aux env = function
 
 let constr_list ist env = constr_list_aux env ist.lfun
 
+(* Extract the identifier list from lfun *)
+let rec extract_ids = function
+  | (id,VIdentifier id')::tl -> id'::extract_ids tl
+  | _::tl -> extract_ids tl
+  | [] -> []
+
 let retype_list sigma env lst =
   List.fold_right (fun (x,csr) a ->
     try (x,Retyping.get_judgment_of env sigma csr)::a with
@@ -1266,7 +1272,7 @@ and interp_tacarg ist gl = function
       interp_app ist gl fv largs loc
   | TacFreshId idopt -> 
       let s = match idopt with None -> "H" | Some s -> s in
-      VIdentifier (Tactics.fresh_id [] (id_of_string s) gl)
+      VIdentifier (Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl)
   | Tacexp t -> val_interp ist gl t
   | TacDynamic(_,t) ->
       let tg = (tag t) in
-- 
cgit v1.2.3