aboutsummaryrefslogtreecommitdiff
path: root/grammar/argextend.mlp
AgeCommit message (Expand)Author
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2017-11-02Using a specific function to register vernac printers.Hugo Herbelin
2017-07-26Removing default evar-normalization for ARGUMENT EXTEND.Pierre-Marie Pédrot
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10don't leak unqualified identifiers from the macroMatej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-16Adding support for using grammar entries returning no value in EXTEND.Hugo Herbelin
2017-04-25[location] Remove `Loc.internal_ghost`Emilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-14Fix compilation with camlp5 transitional mode.Maxime Dénès
2017-04-07[camlpX] Remove camlp4 compat layer.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-01Yet another Makefile reform : a unique phase without nasty make tricksPierre Letouzey