diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 17 | ||||
| -rw-r--r-- | pretyping/termops.mli | 3 |
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 - |