From 5645beeab5801e86704c97b2cc8687b01c14acb8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 12 Mar 2021 18:30:09 +0100
Subject: Move the responsibility of type-checking to the caller for
 tactic-in-terms.

Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.

This should be 1:1 equivalent to the previous code, we are just moving code
around.
---
 plugins/ltac/tacinterp.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f2241e78d2..54d7c310aa 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2148,7 +2148,8 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval lfun poly env sigma ty tac =
+  let eval ?loc ~poly env sigma tycon tac =
+    let lfun = GlobEnv.lfun env in
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun; poly; extra; } in
     let tac = eval_tactic_ist ist tac in
@@ -2156,8 +2157,13 @@ let _ =
        poly seems like enough to get reasonable behavior in practice
      *)
     let name = Id.of_string "ltac_gen" in
-    let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
-    (EConstr.of_constr c, sigma)
+    let sigma, ty = match tycon with
+    | Some ty -> sigma, ty
+    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+    in
+    let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in
+    let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in
+    (j, sigma)
   in
   GlobEnv.register_constr_interp0 wit_tactic eval
 
-- 
cgit v1.2.3