aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/extend.mli
Commit message (Expand)AuthorAge
* Higher-level API for tactic notations.Gravatar Pierre-Marie Pédrot2016-04-24
* Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* Allowing generalized rules in typed symbols.Gravatar Pierre-Marie Pédrot2016-03-19
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Separating the parsing of user-defined entries from their intepretation.Gravatar Pierre-Marie Pédrot2016-01-16
* | Fixing the return type of the Atoken symbol.Gravatar Pierre-Marie Pédrot2015-10-28
* | Type-safe grammar extensions.Gravatar Pierre-Marie Pédrot2015-10-27
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Extend become a mli-only file in intf/Gravatar letouzey2012-05-29