diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 3 | ||||
| -rw-r--r-- | pretyping/namegen.ml | 11 | ||||
| -rw-r--r-- | pretyping/namegen.mli | 5 |
3 files changed, 18 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0f71e47fb7..774180c67b 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1537,7 +1537,8 @@ let define_pure_evar_as_lambda env evd evk = | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ | _ -> error_not_product_loc dummy_loc env evd typ in let avoid = ids_of_named_context (evar_context evi) in - let id = next_name_away_with_default "x" na avoid in + let id = + next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in let newenv = push_named (id, None, dom) evenv in let filter = true::evar_filter evi in let src = evar_source evk evd1 in diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index c3c6b205d9..2ad2f3515c 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -205,6 +205,17 @@ let next_name_away_with_default default na avoid = let id = match na with Name id -> id | Anonymous -> id_of_string default in next_ident_away id avoid +let reserved_type_name = ref (fun t -> Anonymous) +let set_reserved_typed_name f = reserved_type_name := f + +let next_name_away_with_default_using_types default na avoid t = + let id = match na with + | Name id -> id + | Anonymous -> match !reserved_type_name t with + | Name id -> id + | Anonymous -> id_of_string default in + next_ident_away id avoid + let next_name_away = next_name_away_with_default "H" let make_all_name_different env = diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 0c9fc4f6b5..637cbf64de 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -59,6 +59,11 @@ val next_name_away : name -> identifier list -> identifier (** default is "H" * val next_name_away_with_default : string -> name -> identifier list -> identifier +val next_name_away_with_default_using_types : string -> name -> + identifier list -> types -> identifier + +val set_reserved_typed_name : (types -> name) -> unit + (********************************************************************* Making name distinct for displaying *) |