Allowing ML objects to return mere tactic expressions.

4 files changed, 21 insertions, 9 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index b8bec37d04..e1aa6eb48c 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -779,7 +779,7 @@ let gtypref kn = GTypRef (Other kn, [])
 
 let intern_constr self ist c =
   let (_, (c, _)) = Genintern.intern Stdarg.wit_constr ist c in
-  (c, gtypref t_constr)
+  (GlbVal c, gtypref t_constr)
 
 let interp_constr flags ist c =
   let open Pretyping in
@@ -821,7 +821,7 @@ let () =
   let interp _ id = return (ValExt (Value.val_ident, id)) in
   let print _ id = str "ident:(" ++ Id.print id ++ str ")" in
   let obj = {
-    ml_intern = (fun _ _ id -> id, gtypref t_ident);
+    ml_intern = (fun _ _ id -> GlbVal id, gtypref t_ident);
     ml_interp = interp;
     ml_subst = (fun _ id -> id);
     ml_print = print;
@@ -831,7 +831,7 @@ let () =
 let () =
   let intern self ist c =
     let _, pat = Constrintern.intern_constr_pattern ist.Genintern.genv ~as_type:false c in
-    pat, gtypref t_pattern
+    GlbVal pat, gtypref t_pattern
   in
   let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in
   let interp _ c = return (ValExt (Value.val_pattern, c)) in
@@ -846,14 +846,14 @@ let () =
 let () =
   let intern self ist qid = match qid with
   | Libnames.Ident (_, id) ->
-    Globnames.VarRef id, gtypref t_reference
+    GlbVal (Globnames.VarRef id), gtypref t_reference
   | Libnames.Qualid (loc, qid) ->
     let gr =
       try Nametab.locate qid
       with Not_found ->
         Nametab.error_global_not_found ?loc qid
     in
-    gr, gtypref t_reference
+    GlbVal gr, gtypref t_reference
   in
   let subst s c = Globnames.subst_global_reference s c in
   let interp _ gr = return (Value.of_reference gr) in
@@ -875,7 +875,7 @@ let () =
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
     let ist = { ist with Genintern.extra } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    tac, gtypref t_unit
+    GlbVal tac, gtypref t_unit
   in
   let interp _ tac =
     (** FUCK YOU API *)
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 56fd55ee84..5a817df713 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -251,10 +251,14 @@ let shortest_qualid_of_projection kn =
   let sp = KNmap.find kn tab.tab_proj_rev in
   KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj
 
+type 'a or_glb_tacexpr =
+| GlbVal of 'a
+| GlbTacexpr of glb_tacexpr
+
 type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
 
 type ('a, 'b) ml_object = {
-  ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b, 'r) intern_fun;
+  ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
   ml_print : Environ.env -> 'b -> Pp.t;
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 15664db756..eb18dc8e39 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -105,10 +105,14 @@ val interp_primitive : ml_tactic_name -> ml_tactic
 
 (** {5 ML primitive types} *)
 
+type 'a or_glb_tacexpr =
+| GlbVal of 'a
+| GlbTacexpr of glb_tacexpr
+
 type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
 
 type ('a, 'b) ml_object = {
-  ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b, 'r) intern_fun;
+  ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
   ml_print : Environ.env -> 'b -> Pp.t;
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 5d2fc2b47b..2b234d7aec 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -789,7 +789,11 @@ let rec intern_rec env = function
   let ist = empty_glob_sign genv in
   let ist = { ist with extra = Store.set ist.extra ltac2_env env } in
   let arg, tpe = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> obj.ml_intern self ist arg) () in
-  (GTacExt (tag, arg), tpe)
+  let e = match arg with
+  | GlbVal arg -> GTacExt (tag, arg)
+  | GlbTacexpr e -> e
+  in
+  (e, tpe)
 
 and intern_rec_with_constraint env e exp =
   let loc = loc_of_tacexpr e in