From 7f562a9539522e56004596a751758a08cee798b1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Aug 2017 16:58:06 +0200
Subject: Allowing calls to Ltac2 inside Ltac1.

---
 src/tac2core.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index b95410f40e..118bea0f8e 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -765,6 +765,26 @@ let () =
   in
   Pretyping.register_constr_interp0 wit_ltac2 interp
 
+(** Ltac2 in Ltac1 *)
+
+let () =
+  (** FUCK YOU API *)
+  let e = (Obj.magic Tac2entries.Pltac.tac2expr : _ API.Pcoq.Gram.entry) in
+  let inject (loc, v) = Tacexpr.TacGeneric (in_gen (rawwit wit_ltac2) v) in
+  Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None)
+
+let () =
+  let open Ltac_plugin in
+  let open Tacinterp in
+  let idtac = Value.of_closure (default_ist ()) (Tacexpr.TacId []) in
+  (** FUCK YOU API *)
+  let idtac = (Obj.magic idtac : Geninterp.Val.t) in
+  let interp ist tac =
+    Tac2interp.interp Tac2interp.empty_environment tac >>= fun _ ->
+    Ftactic.return idtac
+  in
+  Geninterp.register_interp0 wit_ltac2 interp
+
 (** Patterns *)
 
 let () =
-- 
cgit v1.2.3