Add a type of untyped term to Ltac's value.

It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218.

The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.

4 files changed, 13 insertions, 5 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index c25e02c02..cb980f5a3 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -47,6 +47,8 @@ let wit_constr = unsafe_of_type ConstrArgType
 
 let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
 
+let wit_uconstr = Genarg.make0 None "uconstr"
+
 let wit_open_constr = unsafe_of_type OpenConstrArgType
 
 let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
@@ -65,4 +67,5 @@ let () =
   register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
   register_name0 wit_tactic "Constrarg.wit_tactic";
   register_name0 wit_sort "Constrarg.wit_sort";
+  register_name0 wit_uconstr "Constrarg.uconstr";
   register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 983163ec1..a97ccb270 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -50,6 +50,8 @@ val wit_constr_may_eval :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
   constr) genarg_type
 
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.glob_constr) genarg_type
+
 val wit_open_constr :
   (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7ca4d70c3..5d77c4669 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -638,7 +638,7 @@ let string_of_ty = function
   | Variable -> "var"
 
 let intern_var genv (ltacvars,ntnvars) namedctx loc id =
-  let (ltacvars,unbndltacvars) = ltacvars in
+  let (ltacvars,unbndltacvars,ltacsubst) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
@@ -652,6 +652,9 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars
   then
     GVar (loc,id), [], [], []
+  (* Is [id] bound to a glob_constr in the the ltac context *)
+  else if Id.Map.mem id ltacsubst then
+    Id.Map.find id ltacsubst, [], [], []
   (* Is [id] a notation variable *)
   else if Id.Map.mem id ntnvars
   then
@@ -1549,7 +1552,7 @@ let internalize globalenv env allow_patvar lvar c =
         let solve = match solve with
         | None -> None
         | Some gen ->
-          let ((cvars, lvars), ntnvars) = lvar in
+          let ((cvars, lvars,_), ntnvars) = lvar in
           let ntnvars = Id.Map.domain ntnvars in
           let lvars = Id.Set.union lvars cvars in
           let lvars = Id.Set.union lvars ntnvars in
@@ -1769,9 +1772,9 @@ let scope_of_type_kind = function
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
-type ltac_sign = Id.Set.t * Id.Set.t
+type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t
 
-let empty_ltac_sign = (Id.Set.empty, Id.Set.empty)
+let empty_ltac_sign = (Id.Set.empty, Id.Set.empty, Id.Map.empty)
 
 let intern_gen kind env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 1331fd968..2b61c51dc 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -67,7 +67,7 @@ val compute_internalization_env : env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = Id.Set.t * Id.Set.t
+type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t
 
 type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)