Added a table for using reserved names for binding names to types

(in addition of types to names)

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

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 *)