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.

12 files changed, 83 insertions, 11 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)
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 1375552c3..99e151e38 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -174,6 +174,10 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
+  | UConstr        of 'trm  (* We can reuse ['trm] because terms and untyped terms
+                               only differ at interpretation time (and not at
+                               internalisation), and the output of interpration
+                               is not a variant of [tactic_expr]. *)
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg list
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e10ed49ed..2ceda4f48 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
-    ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty) c
+    ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty,Id.Map.empty) c
 
 (*
    Construct a fixpoint as a Glob_term
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 381534d6d..7fc214304 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -938,6 +938,7 @@ and pr_tacarg = function
   | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
   | Reference r -> pr_ref r
   | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c
+  | UConstr c -> str"uconstr:" ++ pr_constr c
   | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
   | TacExternal (_,com,req,la) ->
       str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 95c6b6bfb..2c36398ed 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -46,6 +46,14 @@ let to_constr v =
     match vars with [] -> Some c | _ -> None
   else None
 
+let of_uconstr c = in_gen (topwit wit_uconstr) c
+
+let to_uconstr v =
+  let v = normalize v in
+  if has_type v (topwit wit_uconstr) then
+    Some (out_gen (topwit wit_uconstr) v)
+  else None
+
 let of_int i = in_gen (topwit wit_int) i
 
 let to_int v =
@@ -139,6 +147,14 @@ let coerce_to_constr env v =
     (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
+let coerce_to_uconstr env v =
+  let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "an untyped term") in
+  if has_type v (topwit wit_uconstr) then
+    out_gen (topwit wit_uconstr) v
+  else
+    fail ()
+
 let coerce_to_closed_constr env v =
   let ids,c = coerce_to_constr env v in
   let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 75f45e731..b4c0283c9 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -37,6 +37,8 @@ sig
 
   val of_constr : constr -> t
   val to_constr : t -> constr option
+  val of_uconstr : Glob_term.glob_constr -> t
+  val to_uconstr : t -> Glob_term.glob_constr option
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
@@ -56,6 +58,8 @@ val coerce_to_int : Value.t -> int
 
 val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
 
+val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.glob_constr
+
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
 val coerce_to_evaluable_ref :
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c624a38d1..44b695e21 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -245,7 +245,7 @@ let intern_binding_name ist x =
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
-  let ltacvars = (lfun, Id.Set.empty) in
+  let ltacvars = (lfun, Id.Set.empty,Id.Map.empty) in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
   in
@@ -318,7 +318,7 @@ let intern_flag ist red =
 let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 
 let intern_constr_pattern ist ~as_type ~ltacvars pc =
-  let ltacvars = ltacvars, Id.Set.empty in
+  let ltacvars = ltacvars, Id.Set.empty,Id.Map.empty in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.genv ~as_type ~ltacvars pc
   in
@@ -631,7 +631,7 @@ and intern_tactic_as_arg loc onlytac ist a =
   | TacCall _ | TacExternal _ | Reference _
   | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
-  | ConstrMayEval _ | TacFreshId _ as a ->
+  | ConstrMayEval _ | UConstr _ | TacFreshId _ as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
   | MetaIdArg _ -> assert false
 
@@ -646,6 +646,7 @@ and intern_tactic_fun ist (var,body) =
 and intern_tacarg strict onlytac ist = function
   | Reference r -> intern_non_tactic_reference strict ist r
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
+  | UConstr c -> UConstr (intern_constr ist c)
   | MetaIdArg (loc,istac,s) ->
       (* $id can occur in Grammar tactic... *)
       let id = Id.of_string s in
@@ -786,6 +787,9 @@ let () =
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s))
 
+let () =
+  Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c))
+
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b83775b93..cb63d53dd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -453,6 +453,29 @@ let interp_fresh_id ist env l =
       Id.of_string s in
   Tactics.fresh_id_in_env avoid id env
 
+
+
+(* Extract the uconstr list from lfun *)
+let extract_ltac_uconstr_values ist env =
+  let fold id v accu =
+    try
+      let c = coerce_to_uconstr env v in
+      Id.Map.add id c accu
+    with CannotCoerceTo _ -> accu
+  in
+  Id.Map.fold fold ist.lfun Id.Map.empty
+
+(** Significantly simpler than [interp_constr], to interpret an
+    untyped constr, it suffices to substitute any bound Ltac variables
+    while redoint internalisation. *)
+let interp_uconstr ist env = function
+  | (c,None) -> c
+  | (_,Some ce) ->
+      let ltacvars = extract_ltac_uconstr_values ist env in
+      let bndvars = Id.Map.domain ist.lfun in
+      let ltacdata = (Id.Set.empty, bndvars , ltacvars) in
+      intern_gen WithoutTypeConstraint ~ltacvars:ltacdata env ce
+
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_values ist env in
   let vars = (constrvars, ist.lfun) in
@@ -464,7 +487,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   | Some c ->
       let ltacvars = Id.Map.domain constrvars in
       let bndvars = Id.Map.domain ist.lfun in
-      let ltacdata = (ltacvars, bndvars) in
+      let ltacdata = (ltacvars, bndvars,Id.Map.empty) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata env c
   in
   let trace =
@@ -1090,6 +1113,11 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t =
         Proofview.V82.tclEVARS sigma <*>
         GTac.return (Value.of_constr c_interp)
       end
+  | UConstr c ->
+      GTac.raw_enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        GTac.return (Value.of_uconstr (interp_uconstr ist env c))
+      end
   | MetaIdArg (loc,_,id) -> assert false
   | TacCall (loc,r,[]) ->
       interp_ltac_reference loc true ist r
@@ -2024,6 +2052,11 @@ let () =
   in
   Geninterp.register_interp0 wit_tactic interp
 
+let () =
+  Geninterp.register_interp0 wit_uconstr (fun ist gl c ->
+     project gl , interp_uconstr ist (pf_env gl) c
+  )
+
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0d8923d5b..0872f8bbf 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -254,6 +254,7 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 and subst_tacarg subst = function
   | Reference r -> Reference (subst_reference subst r)
   | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
+  | UConstr c -> UConstr (subst_glob_constr subst c)
   | MetaIdArg (_loc,_,_) -> assert false
   | TacCall (_loc,f,l) ->
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
@@ -320,6 +321,7 @@ let () =
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
   Genintern.register_subst0 wit_sort (fun _ v -> v);
-  Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v)
+  Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
+  Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c)
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic