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

5 files changed, 23 insertions, 26 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 13983126ad..a36be94fcd 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -693,6 +693,23 @@ 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 allow_secvar id avoid = 
+  let rec next_rec id =
+    let id = next_ident_away_from id avoid in
+    if (allow_secvar && 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 allow_secvar id avoid =
+  let id  = next_ident_away id avoid in
+  if (allow_secvar && is_section_variable id) || not (is_global id) then
+    id
+  else  
+    next_global_ident_from allow_secvar (lift_ident id) avoid
+
 (* Nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 0f970706a3..317a375632 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -153,6 +153,8 @@ type used_idents = identifier list
 val occur_rel : int -> name list -> identifier -> bool
 val occur_id : name list -> identifier -> constr -> bool
 
+val next_global_ident_away : 
+  (*allow section vars:*) bool -> identifier -> identifier list -> identifier
 val next_name_not_occuring :
   bool -> name -> identifier list -> name list -> constr -> identifier
 val concrete_name :
@@ -183,4 +185,3 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Test if an identifier is the basename of a global reference *)
 val is_global : identifier -> bool
-
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