Using a dedicated argument for tactic quotations.

This prevents having to go through an expensive phase of goal-building, when
we can simply type-check the term.

5 files changed, 46 insertions, 2 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 5c285010e9..7295f31181 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -717,8 +717,8 @@ GEXTEND Gram
         let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
         CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
       | test_dollar_ident; "$"; id = Prim.ident ->
-        let tac = Tac2quote.of_exact_var ~loc:!@loc (Loc.tag ~loc:!@loc id) in
-        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+        let id = Loc.tag ~loc:!@loc id in
+        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
         CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
     ] ]
   ;
diff --git a/src/tac2core.ml b/src/tac2core.ml
index f969183dce..8b83e501f9 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -912,6 +912,23 @@ let () =
   in
   Pretyping.register_constr_interp0 wit_ltac2 interp
 
+let () =
+  let interp ist env sigma concl id =
+    let ist = Tac2interp.get_env ist in
+    let c = Id.Map.find id ist.env_ist in
+    let c = Value.to_constr c in
+    let evdref = ref sigma in
+    let () = Typing.e_check env evdref c concl in
+    (c, !evdref)
+  in
+  Pretyping.register_constr_interp0 wit_ltac2_quotation interp
+
+let () =
+  let pr_raw id = mt () in
+  let pr_glb id = str "$" ++ Id.print id in
+  let pr_top _ = mt () in
+  Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top
+
 (** Ltac2 in Ltac1 *)
 
 let () =
diff --git a/src/tac2env.ml b/src/tac2env.ml
index ef2b44afb9..831c6a3b42 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -276,6 +276,7 @@ let std_prefix =
 (** Generic arguments *)
 
 let wit_ltac2 = Genarg.make0 "ltac2:value"
+let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
 
 let is_constructor qid =
   let (_, id) = repr_qualid qid in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 49c9910a44..89e22f07d5 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -132,6 +132,7 @@ val std_prefix : ModPath.t
 (** {5 Generic arguments} *)
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
+val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
 
 (** {5 Helper functions} *)
 
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 2dcd8b8da3..0efd9a3005 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -25,6 +25,7 @@ let t_int = coq_type "int"
 let t_string = coq_type "string"
 let t_array = coq_type "array"
 let t_list = coq_type "list"
+let t_constr = coq_type "constr"
 
 let c_nil = GTacCst (Other t_list, 0, [])
 let c_cons e el = GTacCst (Other t_list, 0, [e; el])
@@ -1511,3 +1512,27 @@ let () =
   in
   Genintern.register_intern0 wit_ltac2 intern
 let () = Genintern.register_subst0 wit_ltac2 subst_expr
+
+let () =
+  let open Genintern in
+  let intern ist (loc, id) =
+    let env = match Genintern.Store.get ist.extra ltac2_env with
+    | None ->
+      (** Only happens when Ltac2 is called from a constr or ltac1 quotation *)
+      let env = empty_env () in
+      if !Ltac_plugin.Tacintern.strict_check then env
+      else { env with env_str = false }
+    | Some env -> env
+    in
+    let t =
+      try Id.Map.find id env.env_var
+      with Not_found ->
+        CErrors.user_err ?loc (str "Unbound value " ++ Id.print id)
+    in
+    let t = fresh_mix_type_scheme env t in
+    let () = unify ?loc env t (GTypRef (Other t_constr, [])) in
+    (ist, id)
+  in
+  Genintern.register_intern0 wit_ltac2_quotation intern
+
+let () = Genintern.register_subst0 wit_ltac2_quotation (fun _ id -> id)