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