| Age | Commit message (Expand) | Author |
|---|
| 2016-05-03 | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug. | Matej Kosik |
| 2016-05-02 | Generate parsing rules for ML tactics in the same order as before a7917a32. | Pierre-Marie Pédrot |
| 2016-05-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-02 | Useless code in Tacentries. | Pierre-Marie Pédrot |
| 2016-04-29 | Reduce ide/coq.png to 256x256. | Guillaume Melquiond |
| 2016-04-29 | Fix incorrect cbv reduction of primitive projections. (Bug #4634) | Guillaume Melquiond |
| 2016-04-28 | Make the language grammar much more precise. (Fix bugs #4682 and #4683) | Guillaume Melquiond |
| 2016-04-28 | Update tutorial (fix bug #4699). | Guillaume Melquiond |
| 2016-04-28 | Fix missing newline in coqchk engagement (bug #4694). | Guillaume Melquiond |
| 2016-04-28 | An example for cd139311e, showing a consequence of not converting | Hugo Herbelin |
| 2016-04-27 | Revert "A heuristic to add parentheses in the presence of rules such as" | Hugo Herbelin |
| 2016-04-27 | Revert "Not taking arguments given by name or position into account when" | Hugo Herbelin |
| 2016-04-27 | Revert "Adding a target for beautification." | Hugo Herbelin |
| 2016-04-27 | Revert "Adding a target check-beautify for testing reparsability of" | Hugo Herbelin |
| 2016-04-27 | Revert "So as to beautify to work, do not use notations in Inductive types" | Hugo Herbelin |
| 2016-04-27 | Revert "Protect the beautifier from change in the lexer state (typically by" | Hugo Herbelin |
| 2016-04-27 | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it" | Hugo Herbelin |
| 2016-04-27 | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin |
| 2016-04-27 | Revert "Being defensive in printing implicit arguments also with manual" | Hugo Herbelin |
| 2016-04-27 | Revert "Temporary deactivate re-interpretation of terms in beautify." | Hugo Herbelin |
| 2016-04-27 | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and" | Hugo Herbelin |
| 2016-04-27 | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an" | Hugo Herbelin |
| 2016-04-27 | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ... | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printers for pr_auto_using and pr_firstorder_using." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of pat%constr." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of induction/destruct as." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing extra space in printing destruct/induction as." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of inversion as." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of keeping hyp on the fly." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing parsing of constr argument of ltac functions at level 8 in the" | Hugo Herbelin |
| 2016-04-27 | Revert "Protect printing of intro-patterns from collision when "[|" or "|]"" | Hugo Herbelin |
| 2016-04-27 | Revert "Protect printing of ltac's "context [...]" from possible collision" | Hugo Herbelin |
| 2016-04-27 | Revert "Revert "Protect printing of intro-patterns from collision when "[|" or" | Hugo Herbelin |
| 2016-04-27 | Revert "Printing notations as parsed." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of Arguments." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of Polymorphic/Monomorphic." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of Instance." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing extra space in printing bullets." | Hugo Herbelin |
| 2016-04-27 | Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco... | Hugo Herbelin |
| 2016-04-27 | Revert "Simplification in ppvernac.ml." | Hugo Herbelin |
| 2016-04-27 | Revert "Isolating and exporting a function for printing body of a recursive d... | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of Function." | Hugo Herbelin |
| 2016-04-27 | Revert "Adding printers for ring and field commands." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing Add Parametric Relation by adding printer for binders." | Hugo Herbelin |
| 2016-04-27 | Revert "Fixing printing of Register retroknowledge." | Hugo Herbelin |
| 2016-04-27 | Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a" | Hugo Herbelin |
| 2016-04-27 | Revert "Passing around the precedence to the generic printer so as to solve" | Hugo Herbelin |
| 2016-04-27 | Revert "Temporary hack to compensate missing comma while re-printing tactic" | Hugo Herbelin |
