From ba61b133772d76e6ff3f93da2ab136afd2f5a867 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Sep 2017 18:23:17 +0200
Subject: Allowing ML objects to return mere tactic expressions.

---
 src/tac2intern.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src/tac2intern.ml')

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
-- 
cgit v1.2.3