Library MetaRocq.Template.Loader

From MetaRocq.Common Require BasicAst.

From MetaRocq.Template Require TemplateMonad.Core TemplateMonad.Extractable Ast Constants.

Declare ML Module "rocq-metarocq-template-rocq.plugin".

Notation "<% x %>" := (ltac:(let p y := exact y in quote_term x p))
  (only parsing).

Notation "<# x #>" := (match TemplateMonad.Core.tmQuoteRec x return _ with qx ⇒ ltac:(let p y := exact y in run_template_program qx p) end)
  (only parsing).