3 files changed, 24 insertions, 18 deletions
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 34fae613bf..ad28b54900 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -51,6 +51,8 @@ let make ~hypnaming env sigma lvar =
   }
 
 let env env = env.static_env
+let renamed_env env = env.renamed_env
+let lfun env = env.lvar.ltac_genargs
 
 let vars_of_env env =
   Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env)
@@ -183,10 +185,13 @@ let interp_ltac_variable ?loc typing_fun env sigma id : Evd.evar_map * unsafe_ju
 
 let interp_ltac_id env id = ltac_interp_id env.lvar id
 
+type 'a obj_interp_fun =
+  ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
+  'a -> unsafe_judgment * Evd.evar_map
+
 module ConstrInterpObj =
 struct
-  type ('r, 'g, 't) obj =
-    unbound_ltac_var_map -> bool -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+  type ('r, 'g, 't) obj = 'g obj_interp_fun
   let name = "constr_interp"
   let default _ = None
 end
@@ -195,8 +200,8 @@ module ConstrInterp = Genarg.Register(ConstrInterpObj)
 
 let register_constr_interp0 = ConstrInterp.register0
 
-let interp_glob_genarg env poly sigma ty arg =
+let interp_glob_genarg ?loc ~poly env sigma ty arg =
   let open Genarg in
   let GenArg (Glbwit tag, arg) = arg in
   let interp = ConstrInterp.obj tag in
-  interp env.lvar.ltac_genargs poly env.renamed_env sigma ty arg
+  interp ?loc ~poly env sigma ty arg
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 023e24e6d8..40feb8206b 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -15,11 +15,18 @@ open EConstr
 open Ltac_pretype
 open Evarutil
 
+(** Type of environment extended with naming and ltac interpretation data *)
+
+type t
+
 (** To embed constr in glob_constr *)
 
+type 'a obj_interp_fun =
+  ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
+  'a -> unsafe_judgment * Evd.evar_map
+
 val register_constr_interp0 :
-  ('r, 'g, 't) Genarg.genarg_type ->
-    (unbound_ltac_var_map -> bool -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+  ('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit
 
 (** {6 Pretyping name management} *)
 
@@ -32,10 +39,6 @@ val register_constr_interp0 :
       variables used to build purely-named evar contexts
 *)
 
-(** Type of environment extended with naming and ltac interpretation data *)
-
-type t
-
 (** Build a pretyping environment from an ltac environment *)
 
 val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
@@ -43,6 +46,8 @@ val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
 (** Export the underlying environment *)
 
 val env : t -> env
+val renamed_env : t -> env
+val lfun : t -> unbound_ltac_var_map
 
 val vars_of_env : t -> Id.Set.t
 
@@ -85,5 +90,5 @@ val interp_ltac_id : t -> Id.t -> Id.t
 (** Interpreting a generic argument, typically a "ltac:(...)", taking
     into account the possible renaming *)
 
-val interp_glob_genarg : t -> bool -> evar_map -> constr ->
-  Genarg.glob_generic_argument -> constr * evar_map
+val interp_glob_genarg : ?loc:Loc.t -> poly:bool -> t -> evar_map -> Evardefine.type_constraint ->
+  Genarg.glob_generic_argument -> unsafe_judgment * evar_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3ccc6ea125..800096f2b3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -653,12 +653,8 @@ struct
       sigma, { uj_val; uj_type }
 
     | Some arg ->
-      let sigma, ty =
-        match tycon with
-        | Some ty -> sigma, ty
-        | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in
-      let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
-      sigma, { uj_val = c; uj_type = ty }
+      let j, sigma = GlobEnv.interp_glob_genarg ?loc ~poly env sigma tycon arg in
+      sigma, j
 
   let pretype_rec self (fixkind, names, bl, lar, vdef) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->