1 2 3 4 5
Declare ML Module "ocaml.cmo" "extraction.cmo". Grammar vernac vernac : ast := extr_constr [ "Extraction" constrarg($c) "." ] -> [(Extraction $c)].