Collecting in Namegen those conventional default names that are used in different places

15 files changed, 54 insertions, 29 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7f13fff2cf..475f8d396c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -411,7 +411,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	    let id =
 	      match ty with
 	      | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id
-	      | _ -> Id.of_string "H"
+	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 75ebdeb22b..94ec09db2a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -67,7 +67,7 @@ let rec list_try_compile f = function
 	    list_try_compile f t
 
 let force_name =
-  let nx = Name (Id.of_string "x") in function Anonymous -> nx | na -> na
+  let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
 
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index baa9086166..baf98eee72 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -76,7 +76,6 @@ let app_opt env evdref f t =
   whd_betaiota !evdref (app_opt f t)
 
 let pair_of_array a = (a.(0), a.(1))
-let make_name s = Name (Id.of_string s)
 
 let disc_subset x =
   match kind_of_term x with
@@ -183,7 +182,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	| _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
 	  let name' = 
-	    Name (Namegen.next_ident_away (Id.of_string "x") (Termops.ids_of_context env))
+	    Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env))
 	  in
 	  let env' = push_rel (name', None, a') env in
 	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
@@ -235,7 +234,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		       | _ -> raise NoSubtacCoercion
 		     in
 		     let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
-		     let env' = push_rel (make_name "x", None, a) env in
+		     let env' = push_rel (Name Namegen.default_dependent_ident, None, a) env in
 		     let c2 = coerce_unify env' b b' in
 		       match c1, c2 with
 		       | None, None -> None
@@ -450,7 +449,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
           (* Note: we retype the term because sort-polymorphism may have *)
           (* weaken its type *)
 	  let name = match name with
-	    | Anonymous -> Name (Id.of_string "x")
+	    | Anonymous -> Name Namegen.default_dependent_ident
 	    | _ -> name in
 	  let env1 = push_rel (name,None,u1) env in
 	  let (evd', v1) =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 65a8f338cb..390c3a82e1 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -232,7 +232,7 @@ let rec decomp_branch ndecls nargs nal b (avoid,env as e) c =
 	| LetIn (na,_,_,c) when ndecls>nargs ->
             na,c,compute_displayed_name_in,nargs
 	| _ ->
-	    Name (Id.of_string "x"),(applist (lift 1 c, [mkRel 1])),
+	    Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])),
 	    compute_displayed_name_in,nargs-1 in
     let na',avoid' = f flag avoid na c in
     decomp_branch (ndecls-1) nargs' (na'::nal) b (avoid',add_name na' env) c
@@ -296,7 +296,7 @@ let it_destRLambda_or_LetIn_names n c =
       | _ ->
           (* eta-expansion *)
 	  let next l =
-	    let x = next_ident_away (Id.of_string "x") l in
+	    let x = next_ident_away default_dependent_ident l in
 	    (* Not efficient but unusual and no function to get free glob_vars *)
 (* 	    if occur_glob_constr x c then next (x::l) else x in *)
 	    x
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 18c91c0e30..dc8199ffe7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -680,7 +680,7 @@ let empty_valcon = None
 (* Builds a value constraint *)
 let mk_valcon c = Some c
 
-let idx = Id.of_string "x"
+let idx = Namegen.default_dependent_ident
 
 (* Refining an evar to a product *)
 
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 0581f7283e..6c490d7b9a 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -24,6 +24,24 @@ open Environ
 open Termops
 
 (**********************************************************************)
+(* Conventional names *)
+
+let default_prop_string = "H"
+let default_prop_ident = Id.of_string default_prop_string
+
+let default_small_string = "H"
+let default_small_ident = Id.of_string default_small_string
+
+let default_type_string = "X"
+let default_type_ident = Id.of_string default_type_string
+
+let default_non_dependent_string = "H"
+let default_non_dependent_ident = Id.of_string default_non_dependent_string
+
+let default_dependent_string = "x"
+let default_dependent_ident = Id.of_string "x"
+
+(**********************************************************************)
 (* Globality of identifiers *)
 
 let is_imported_modpath = function
@@ -147,8 +165,6 @@ let it_mkLambda_or_LetIn_name env b hyps =
 (**********************************************************************)
 (* Fresh names *)
 
-let default_x = Id.of_string "x"
-
 (* Looks for next "good" name by lifting subscript *)
 
 let next_ident_away_from id bad =
@@ -173,7 +189,7 @@ let rec to_avoid id = function
 (* 1- Looks for a fresh name for printing in cases pattern *)
 
 let next_name_away_in_cases_pattern na avoid =
-  let id = match na with Name id -> id | Anonymous -> default_x in
+  let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
   next_ident_away_from id (fun id -> to_avoid id avoid || is_constructor id)
 
 (* 2- Looks for a fresh name for introduction in goal *)
@@ -191,7 +207,9 @@ let next_ident_away_in_goal id avoid =
   next_ident_away_from id bad
 
 let next_name_away_in_goal na avoid =
-  let id = match na with Name id -> id | Anonymous -> Id.of_string "H" in
+  let id = match na with
+    | Name id -> id
+    | Anonymous -> default_non_dependent_ident in
   next_ident_away_in_goal id avoid
 
 (* 3- Looks for next fresh name outside a list that is moreover valid
@@ -229,7 +247,7 @@ let next_name_away_with_default_using_types default na avoid t =
 	| Anonymous -> Id.of_string default in
   next_ident_away id avoid
 
-let next_name_away = next_name_away_with_default "H"
+let next_name_away = next_name_away_with_default default_non_dependent_string
 
 let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
@@ -279,7 +297,7 @@ let next_name_away_for_default_printing env_t na avoid =
       (* In principle, an anonymous name is not dependent and will not be *)
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
-      Id.of_string "H" in
+      default_non_dependent_ident in
   next_ident_away_for_default_printing env_t id avoid
 
 (**********************************************************************)
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 857867f3a9..cb28919967 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -12,6 +12,15 @@ open Context
 open Environ
 
 (*********************************************************************
+   Conventional default names *)
+
+val default_prop_ident : Id.t          (* "H" *)
+val default_small_ident : Id.t         (* "H" *)
+val default_type_ident : Id.t          (* "X" *)
+val default_non_dependent_ident : Id.t (* "H" *)
+val default_dependent_ident : Id.t     (* "x" *)
+
+(*********************************************************************
    Generating "intuitive" names from their type *)
 
 val lowercase_first_char : Id.t -> string
@@ -57,7 +66,9 @@ val next_global_ident_away : Id.t -> Id.t list -> Id.t
 (** Avoid clashing with a constructor name already used in current module *)
 val next_name_away_in_cases_pattern : Name.t -> Id.t list -> Id.t
 
-val next_name_away  : Name.t -> Id.t list -> Id.t (** default is "H" *)
+(** Default is [default_non_dependent_ident] *)
+val next_name_away  : Name.t -> Id.t list -> Id.t
+
 val next_name_away_with_default : string -> Name.t -> Id.t list ->
   Id.t
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 31576391b1..dff1b9772f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -817,7 +817,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	      (fun (n, b, t) ->
 		match n with
                   Name _ -> (n, b, t)
-                | Anonymous -> (Name (Id.of_string "H"), b, t))
+                | Anonymous -> (Name Namegen.default_non_dependent_ident, b, t))
 	      cs.cs_args
 	in
 	let env_c = push_rel_context csgn env in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 150f1c2af6..2d8e935bb5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1170,7 +1170,7 @@ let whd_meta sigma c = match kind_of_term c with
   | Meta p -> (try meta_value sigma p with Not_found -> c)
   | _ -> c
 
-let hid = Id.of_string "H"
+let default_plain_instance_ident = Id.of_string "H"
 
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
@@ -1189,7 +1189,7 @@ let plain_instance s c =
 	    match kind_of_term g with
             | App _ ->
                 let l' = CArray.Fun1.smartmap lift 1 l' in
-                mkLetIn (Name hid,g,t,mkApp(mkRel 1, l'))
+                mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
         | _ -> mkApp (irec n f,l'))
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5693cf2987..8b2532a5ff 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -342,7 +342,7 @@ let reference_eval sigma env = function
    The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1]
 *)
 
-let x = Name (Id.of_string "x")
+let x = Name default_dependent_ident
 
 let make_elim_fun (names,(nbfix,lv,n)) u largs =
   let lu = List.firstn n largs in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 08354ef556..d5086df1a3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -313,7 +313,7 @@ let name_prop_vars env sigma ctxt =
   List.map2 (fun (na,b,t as d) s ->
     if na = Anonymous && s = prop_sort then
       let s = match Namegen.head_name t with Some id -> string_of_id id | None -> "" in
-      (Name (add_suffix (id_of_string "H") s),b,t)
+      (Name (add_suffix Namegen.default_prop_ident s),b,t)
     else
       d)
     ctxt (sorts_of_context env sigma ctxt)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index ab2a165757..bcf5e29476 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -888,7 +888,7 @@ type hints_entry =
   | HintsExternEntry of
       int * (patvar list * constr_pattern) option * glob_tactic_expr
 
-let h = Id.of_string "H"
+let default_prepare_hint_ident = Id.of_string "H"
 
 exception Found of constr * types
 
@@ -915,7 +915,7 @@ let prepare_hint check env init (sigma,c) =
   let rec iter c =
     try find_next_evar c; c
     with Found (evar,t) ->
-      let id = next_ident_away_from h (fun id -> Id.Set.mem id !vars) in
+      let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index abf1c47d84..1e88456f36 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -482,7 +482,7 @@ let rec decompose_app_rel env evd t =
       else 
 	let (f', args) = decompose_app_rel env evd args.(0) in
 	let ty = Typing.type_of env evd args.(0) in
-	let f'' = mkLambda (Name (Id.of_string "x"), ty,
+	let f'' = mkLambda (Name default_dependent_ident, ty,
 	  mkLambda (Name (Id.of_string "y"), lift 1 ty,
 	    mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
 	in (f'', args)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index afd077e64a..e08ae998b4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -432,11 +432,8 @@ let id_of_name_with_default id = function
   | Anonymous -> id
   | Name id   -> id
 
-let hid = Id.of_string "H"
-let xid = Id.of_string "X"
-
 let default_id_of_sort s =
-  if Sorts.is_small s then hid else xid
+  if Sorts.is_small s then default_small_ident else default_type_ident
 
 let default_id env sigma = function
   | (name,None,t) ->
diff --git a/toplevel/class.ml b/toplevel/class.ml
index eedb35acf8..9ca75d1737 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -188,7 +188,7 @@ let build_id_coercion idf_opt source poly =
   let lams,t = decompose_lam_assum c in
   let val_f =
     it_mkLambda_or_LetIn
-      (mkLambda (Name (Id.of_string "x"),
+      (mkLambda (Name Namegen.default_dependent_ident,
 		 applistc vs (extended_rel_list 0 lams),
 		 mkRel 1))
        lams