Interoperability with Ltac2

Tactics in Camltac can be exposed to Ltac2 using the FFI module:

Require Import Ltac2.Ltac2.
[Loading ML file rocq-runtime.plugins.ltac2_ltac1 ... done]

Camltac Run ocaml:{{
  (* We expose our previously defined reification procedure to Ltac2: *)
  Ltac2.FFI.(define "reify"
              (constr @-> tac constr)
              Reify.reify)
}}.

Ltac2 @external reify : constr -> constr :=
  "rocq-camltac.plugin.runtime" "reify".

Ltac2 Eval (reify constr:(2 * 3)).
- : constr =
constr:(NatMul (NatSucc (NatSucc NatZero))
          (NatSucc (NatSucc (NatSucc NatZero))))