| Commit message (Expand) | Author | Age |
* | Fix #5174: Underinformative syntax error messages in the new arguments syntax | Maxime Dénès | 2016-11-30 |
* | Revert "Merge remote-tracking branch 'github/pr/360' into v8.6" | Maxime Dénès | 2016-11-18 |
* | [stm] Remove STM-related vernaculars | Emilio Jesus Gallego Arias | 2016-11-17 |
* | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès | 2016-11-07 |
|\ |
|
* \ | Merge remote-tracking branch 'github/pr/340' into v8.6 | Maxime Dénès | 2016-11-03 |
|\ \ |
|
| | * | Lets Hints/Instances take an optional pattern | Matthieu Sozeau | 2016-11-03 |
* | | | Better Arguments compatibility. | Maxime Dénès | 2016-11-02 |
| |/
|/| |
|
| * | Fix various shortcomings of the warnings infrastructure. | Maxime Dénès | 2016-11-02 |
|/ |
|
* | Complete overhaul of the Arguments vernacular. | Maxime Dénès | 2016-10-27 |
* | Do not add "Append" as a lexer keyword. | Pierre-Marie Pédrot | 2016-10-06 |
* | Revert "Move bullet detection from lexer to parser (bug #5102)." | Guillaume Melquiond | 2016-10-05 |
* | Merge remote-tracking branch 'github/pr/305' into v8.6 | Maxime Dénès | 2016-10-04 |
|\ |
|
* | | Move bullet detection from lexer to parser (bug #5102). | Guillaume Melquiond | 2016-10-02 |
| * | Add command 'Set foo Append "bar"' for appending to an option (bug #5109). | Guillaume Melquiond | 2016-10-01 |
|/ |
|
* | Merge remote-tracking branch 'github/pr/299' into v8.6 | Maxime Dénès | 2016-09-30 |
|\ |
|
* | | Fix bug #4798: compat notations should not modify the parser. | Pierre-Marie Pédrot | 2016-09-29 |
* | | Arguments: cleanup + detect discrepancy rename/implicit (#3753) | Enrico Tassi | 2016-09-29 |
| * | Fix bug #4869, allow Prop, Set, and level names in constraints. | Matthieu Sozeau | 2016-09-29 |
|/ |
|
* | restore compatibility with gallium's camlp4 (broken by commit 8e07227c) | Pierre Letouzey | 2016-07-26 |
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
* | A new infrastructure for warnings. | Maxime Dénès | 2016-06-29 |
* | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre | 2016-06-27 |
* | Adding an only printing flag to notations. | Pierre-Marie Pédrot | 2016-06-07 |
* | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-09 |
|\ |
|
| * | Rename Lexer -> CLexer. | Pierre-Marie Pédrot | 2016-05-09 |
* | | Removing dead code and unused opens. | Pierre-Marie Pédrot | 2016-05-08 |
* | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau | 2016-04-04 |
|\ \ |
|
* | | | Moving the Ltac definition command to an EXTEND based command. | Pierre-Marie Pédrot | 2016-03-20 |
* | | | Moving Print Ltac to an EXTEND based command. | Pierre-Marie Pédrot | 2016-03-20 |
* | | | Moving Tactic Notation to an EXTEND based command. | Pierre-Marie Pédrot | 2016-03-20 |
* | | | Moving the parsing of the Ltac proof mode to G_ltac. | Pierre-Marie Pédrot | 2016-03-19 |
* | | | Moving the proof mode parsing management to Pcoq. | Pierre-Marie Pédrot | 2016-03-19 |
* | | | Moving Autorewrite to Hightatctic. | Pierre-Marie Pédrot | 2016-03-06 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-29 |
|\ \ \
| | |/
| |/| |
|
| * | | Implement support for universe binder lists in Instance and Program Fixpoint/... | Matthieu Sozeau | 2016-01-23 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
|\| | |
|
| * | | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | | | Simplification of grammar_prod_item type. | Pierre-Marie Pédrot | 2016-01-02 |
* | | | ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file | Matej Kosik | 2015-12-18 |
* | | | CLEANUP: Vernacexpr.vernac_expr | Matej Kosik | 2015-12-18 |
|/ / |
|
* | | Allowing empty bound universe variables. | Pierre-Marie Pédrot | 2015-10-08 |
* | | Axioms now support the universe binding syntax. | Pierre-Marie Pédrot | 2015-10-08 |
* | | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | 2015-10-08 |
* | | Record fields accept an optional final semicolon separator. | Pierre-Marie Pédrot | 2015-10-07 |
* | | Univs: Add universe binding lists to definitions | Matthieu Sozeau | 2015-09-14 |
* | | Hacking parser so as to support both [> ... ] and [id]. | Hugo Herbelin | 2015-09-08 |
| * | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross | 2015-08-14 |
|/ |
|
* | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | Lionel Rieg | 2015-06-26 |
* | Granting, undocumentedly, parsing of "Conjectures" as a synonym of | Hugo Herbelin | 2015-06-16 |