4 files changed, 22 insertions, 4 deletions
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 6c629468ba..768ef3cfd9 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -47,6 +47,8 @@ struct
 
 end
 
+module ValTMap = ValT.Map
+
 module ValReprObj =
 struct
   type ('raw, 'glb, 'top) obj = 'top Val.tag
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 492e372adb..ae0b26e594 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -39,6 +39,10 @@ sig
   val inject : 'a tag -> 'a -> t
 
 end
+
+module ValTMap (M : Dyn.TParam) :
+  Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+
 (** Dynamic types for toplevel values. While the generic types permit to relate
     objects at various levels of interpretation, toplevel values are wearing
     their own type regardless of where they came from. This allows to use the
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 2e62b89011..a38c73ed0b 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -376,15 +376,22 @@ let next_name_for_display sigma flags =
   | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in sigma flags avoid na c =
+let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c =
   match na with
-  | Anonymous when noccurn sigma 1 c ->
+  | Anonymous when noccurn_fun sigma 1 c ->
     (Anonymous,avoid)
   | _ ->
     let fresh_id = next_name_for_display sigma flags na avoid in
-    let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
+    let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in
     (idopt, Id.Set.add fresh_id avoid)
 
+let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn
+
+let compute_displayed_name_in_gen f sigma =
+  (* only flag which does not need a constr, maybe to be refined *)
+  let flag = RenamingForGoal in
+  compute_displayed_name_in_gen_poly f sigma flag
+
 let compute_and_force_displayed_name_in sigma flags avoid na c =
   match na with
   | Anonymous when noccurn sigma 1 c ->
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 6fde90a39c..d29b69259f 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -106,10 +106,15 @@ val compute_displayed_name_in :
 val compute_and_force_displayed_name_in :
   evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val compute_displayed_let_name_in :
-  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
 val rename_bound_vars_as_displayed :
   evar_map -> Id.Set.t -> Name.t list -> types -> types
 
+(* Generic function expecting a "not occurn" function *)
+val compute_displayed_name_in_gen :
+  (evar_map -> int -> 'a -> bool) ->
+  evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
+
 (**********************************************************************)
 (* Naming strategy for arguments in Prop when eliminating inductive types *)