aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacinterp.ml
Commit message (Expand)AuthorAge
* [vernac] use a record for the contents of the “deprecated” attributeGravatar Vincent Laporte2018-07-03
* [vernac] Add a “deprecated” attributeGravatar Vincent Laporte2018-07-03
* [vernac] mk_atts: an atts record with default valuesGravatar Vincent Laporte2018-07-03
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [vernac] adds the “program” flag to the “atts” recordGravatar Vincent Laporte2017-12-29
* [vernac] Add polymorphic to the type of vernac interpration options.Gravatar Emilio Jesus Gallego Arias2017-11-27
* [vernac] Start to uniformize type of vernac interpretation.Gravatar Emilio Jesus Gallego Arias2017-11-27
* [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [plugin] Encapsulate modifiers to vernac commands.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [vernac] Increase table size.Gravatar Emilio Jesus Gallego Arias2017-11-19
* provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesGravatar Matej Košík2017-11-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 14:23:48 +0000