Library MetaRocq.TemplatePCUIC.Loader

From MetaRocq.Template Require ExtractableLoader.
From MetaRocq.Template Require Export Loader.
From MetaRocq.TemplatePCUIC.PCUICTemplateMonad Require Core.
From MetaRocq.TemplatePCUIC Require Import TemplateMonadToPCUIC.

Notation eval_pcuic_quotation := eval_pcuic_quotation (only parsing).
#[export] Existing Instance default_eval_pcuic_quotation.

Set Warnings "-notation-overridden".
Notation "<% x %>" := (match @monad_trans return _ with monad_trans ⇒ ltac:(let monad_trans := constr:(monad_trans _) in let p y := exact y in let p y := run_template_program (monad_trans y) p in quote_term x p) end)
  (only parsing).

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