We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 36b893b commit ff1187bCopy full SHA for ff1187b
src/rocq_elpi_builtins.ml
@@ -3387,6 +3387,8 @@ Supported attributes:
3387
let pat, _ = Notation_ops.notation_constr_of_glob_constr nenv gbody in
3388
let warns = warns_of_options options in
3389
Abbreviation.declare_abbreviation ~local ~onlyparsing warns name (vars,pat);
3390
+ let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
3391
+ Dumpglob.dump_definition (CAst.make ~loc name) false "abbrev";
3392
let qname = Libnames.qualid_of_string (Id.to_string name) in
3393
match Nametab.locate_extended qname with
3394
| Globnames.TrueGlobal _ -> assert false
0 commit comments