Deplacement next_global_ident_away dans Termops

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 4 insertions, 25 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index cb2809cd3e..5ca8c35889 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -126,7 +126,7 @@ let replace_in_array env gmm a =
     
 let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_" in
-  next_global_ident_away id (ids_of_named_context (named_context env))
+  next_global_ident_away true id (ids_of_named_context (named_context env))
 
 let rec compute_metamap env gmm c = match kind_of_term c with
   (* le terme est directement une preuve *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 98e36520a8..c4a7e42881 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -227,29 +227,8 @@ let unfold_constr = function
 (*         Introduction tactics            *)
 (*******************************************)
 
-let is_section_variable id =
-  try let _ = Sign.lookup_named id (Global.named_context()) in true
-  with Not_found -> false
-
-let next_global_ident_from id avoid = 
-  let rec next_rec id =
-    let id = next_ident_away_from id avoid in
-    if is_section_variable id || not (is_global id) then
-      id
-    else  
-      next_rec (lift_ident id)
-  in 
-  next_rec id
-
-let next_global_ident_away id avoid =
-  let id  = next_ident_away id avoid in
-  if is_section_variable id || not (is_global id) then
-    id
-  else  
-    next_global_ident_from (lift_ident id) avoid
-
 let fresh_id avoid id gl =
-  next_global_ident_away id (avoid@(pf_ids_of_hyps gl))
+  next_global_ident_away true id (avoid@(pf_ids_of_hyps gl))
 
 let id_of_name_with_default s = function
   | Anonymous -> id_of_string s
@@ -1678,7 +1657,8 @@ let abstract_subproof name tac gls =
 	 if mem_named_context id current_sign then s else add_named_decl d s) 
       global_sign empty_named_context
   in
-  let na = next_global_ident_away name (ids_of_named_context global_sign) in
+  let na =
+    next_global_ident_away false name (ids_of_named_context global_sign) in
   let concl = 
     List.fold_left (fun t d -> mkNamedProd_or_LetIn d t) (pf_concl gls) sign 
   in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1f4c5b35cf..820c20d375 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -55,7 +55,6 @@ val cofix           : identifier option -> tactic
 
 (*s Introduction tactics. *)
 
-val next_global_ident_away : identifier -> identifier list -> identifier
 val fresh_id : identifier list -> identifier -> goal sigma -> identifier
 
 val intro                : tactic