| Age | Commit message (Expand) | Author |
|---|
| 2016-07-03 | Remove lexing of ordinal notations. | Maxime Dénès |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès |
| 2016-06-29 | A new infrastructure for warnings. | Maxime Dénès |
| 2016-06-27 | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre |
| 2016-06-21 | Parsing/compat.ml4: avoid "let open" syntax, unsupported by my camlp5 6.11 | Pierre Letouzey |
| 2016-06-20 | Merge remote-tracking branch 'github/pr/212' into trunk | Maxime Dénès |
| 2016-06-20 | Add file name, line number and beginning of line position to locations. | Maxime Dénès |
| 2016-06-18 | Exporting a generic argument induction_arg. As a consequence, | Hugo Herbelin |
| 2016-06-18 | Adding eintros to respect the e- prefix policy. | Hugo Herbelin |
| 2016-06-17 | Set required version of camlp5 to 6.06. | Maxime Dénès |
| 2016-06-16 | Extend Hint Mode to handle the no-head-evar case | Matthieu Sozeau |
| 2016-06-16 | Fixing a mispelling coma -> comma. | Hugo Herbelin |
| 2016-06-16 | A stronger invariant on the syntax of TacAssert, what allows for a | Hugo Herbelin |
| 2016-06-07 | Adding an only printing flag to notations. | Pierre-Marie Pédrot |
| 2016-06-07 | Removing the use to Egramcoq.recover_constr_grammar. | Pierre-Marie Pédrot |
| 2016-06-03 | Removing "rename" from the tactic AST. | Pierre-Marie Pédrot |
| 2016-06-03 | Removing "exact" from the tactic AST. | Pierre-Marie Pédrot |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot |
| 2016-06-03 | Removing "double induction" from the tactic AST. | Pierre-Marie Pédrot |
| 2016-06-01 | g_tactics : remove opt_bindings (2-line dead code) | Pierre Letouzey |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-05-11 | The grammar_extend function now registers unsynchronized extensions. | Pierre-Marie Pédrot |
| 2016-05-11 | Making the grammar command extend API purely functional. | Pierre-Marie Pédrot |
| 2016-05-11 | Moving the constr empty entry registering to the state-based API. | Pierre-Marie Pédrot |
| 2016-05-11 | Turning the grammar extend command API into a state-passing one. | Pierre-Marie Pédrot |
| 2016-05-11 | Moving the grammar summary to Pcoq. | Pierre-Marie Pédrot |
| 2016-05-10 | Delimiting the use of unsafe code in Pcoq. | Pierre-Marie Pédrot |
| 2016-05-10 | Overlooked use of Gram instead of G module in Pcoq. | Pierre-Marie Pédrot |
| 2016-05-10 | Further tidying of the constr extension code. | Pierre-Marie Pédrot |
| 2016-05-10 | Type-safe constr notations. | Pierre-Marie Pédrot |
| 2016-05-10 | AlistNsep token now accepts an arbitrary separator. | Pierre-Marie Pédrot |
| 2016-05-10 | Simpler data structure for Arules token. | Pierre-Marie Pédrot |
| 2016-05-10 | Purer implementation of empty level registering in Pcoq. | Pierre-Marie Pédrot |
| 2016-05-10 | Removing the Entry module now that rules need not be marshalled. | Pierre-Marie Pédrot |
| 2016-05-10 | Hardening the obsolete unsafe_grammar_statement API. | Pierre-Marie Pédrot |
| 2016-05-10 | Removing dead code in Compat. | Pierre-Marie Pédrot |
| 2016-05-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-09 | Rename Lexer -> CLexer. | Pierre-Marie Pédrot |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot |
| 2016-05-04 | Removing useless generic arguments. | Pierre-Marie Pédrot |
| 2016-04-27 | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing a mispelling coma -> comma." | Hugo Herbelin |
| 2016-04-27 | Fixing a mispelling coma -> comma. | Hugo Herbelin |
| 2016-04-27 | In the short term, stronger invariant on the syntax of TacAssert, what | Hugo Herbelin |
| 2016-04-25 | Removing dead code in Compat. | Pierre-Marie Pédrot |
| 2016-04-24 | Remove dead registering code in Pcoq. | Pierre-Marie Pédrot |
| 2016-04-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-04-12 | A fix to #4666 (Exc_located capsule added by camlp5 overwriting | Hugo Herbelin |
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau |
