Allowing to insert calls to Ltac1 references in Ltac2.

3 files changed, 30 insertions, 0 deletions

diff --git a/doc/ltac2.md b/doc/ltac2.md
index a645331e2d..51e3ab664d 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -692,6 +692,17 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0)
 Note that abbreviations are not typechecked at all, and may result in typing
 errors after expansion.
 
+# Compatibility layer with Ltac1
+
+## Ltac1 from Ltac2
+
+One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses
+a Ltac1 expression, and semantics of this quotation is the evaluation of the
+corresponding code for its side effects.
+
+Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
+to the use of standalone function calls.
+
 # Transition from Ltac1
 
 Owing to the use of a bunch of notations, the transition shouldn't be
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index e7ab574747..6822b8e7ba 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -72,10 +72,14 @@ let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
 let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
+(** FUCK YOU API *)
+let ltac1_expr = (Obj.magic Pltac.tactic_expr : Tacexpr.raw_tactic_expr Gram.entry)
+
 let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
 let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
 let inj_pattern loc c = inj_wit Tac2env.wit_pattern loc c
 let inj_reference loc c = inj_wit Tac2env.wit_reference loc c
+let inj_ltac1 loc e = inj_wit Tacarg.wit_tactic loc e
 
 let pattern_of_qualid loc id =
   if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
@@ -170,6 +174,7 @@ GEXTEND Gram
       | IDENT "ident"; ":"; "("; c = lident; ")" -> Tac2quote.of_ident c
       | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> inj_pattern !@loc c
       | IDENT "reference"; ":"; "("; c = globref; ")" -> inj_reference !@loc c
+      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr; ")" -> inj_ltac1 !@loc qid
     ] ]
   ;
   let_clause:
diff --git a/src/tac2core.ml b/src/tac2core.ml
index b67d70a5cb..b95410f40e 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -738,6 +738,20 @@ let () =
   define_ml_object Tac2env.wit_reference obj
 
 let () =
+  let interp _ tac =
+    (** FUCK YOU API *)
+    (Obj.magic Ltac_plugin.Tacinterp.eval_tactic tac : unit Proofview.tactic) >>= fun () ->
+    return v_unit
+  in
+  let obj = {
+    ml_type = t_unit;
+    ml_interp = interp;
+  } in
+  define_ml_object Ltac_plugin.Tacarg.wit_tactic obj
+
+(** Ltac2 in terms *)
+
+let () =
   let interp ist env sigma concl tac =
     let fold id (Val.Dyn (tag, v)) (accu : environment) : environment =
       match Val.eq tag val_valexpr with