diff options
| author | herbelin | 2003-10-21 08:53:20 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-21 08:53:20 +0000 |
| commit | 505df17983e546305278c6332e5976d751c01b9b (patch) | |
| tree | 2a7ad0ccf869e9c3cc6c2909d32e06313c8ad9a3 | |
| parent | 69b0bfdbe4440805840fa00eb5d9714b844dc178 (diff) | |
Correction bug FreshId
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4683 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 10 |
1 files 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 |