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

2 files changed, 19 insertions, 1 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
-