aboutsummaryrefslogtreecommitdiff
path: root/intf/extend.ml
AgeCommit message (Expand)Author
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-03-08Make most of TACTIC EXTEND macros runtime calls.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20Notations: A step in cleaning constr_entry_key.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Hugo Herbelin
2018-02-20Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-07Put all plugins behind an "API".Matej Kosik