| Age | Commit message (Expand) | Author |
|---|
| 2017-01-21 | Revert "Process Next Obligation proofs in parallel (fix #5314)" | Enrico Tassi |
| 2017-01-20 | Process Next Obligation proofs in parallel (fix #5314) | Enrico Tassi |
| 2016-11-18 | Revert "Merge remote-tracking branch 'github/pr/360' into v8.6" | Maxime Dénès |
| 2016-11-17 | [stm] Remove STM-related vernaculars | Emilio Jesus Gallego Arias |
| 2016-11-03 | Lets Hints/Instances take an optional pattern | Matthieu Sozeau |
| 2016-10-27 | Complete overhaul of the Arguments vernacular. | Maxime Dénès |
| 2016-10-04 | Quick fix to #4595 (making notations containing "ltac:" unused for printing). | Hugo Herbelin |
| 2016-10-01 | Add command 'Set foo Append "bar"' for appending to an option (bug #5109). | Guillaume Melquiond |
| 2016-09-30 | Merge remote-tracking branch 'github/pr/299' into v8.6 | Maxime Dénès |
| 2016-09-29 | 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-08-27 | Support qualified identifiers in Show Match (bug #5050). | Guillaume Melquiond |
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès |
| 2016-06-27 | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre |
| 2016-06-20 | COMMENTS: Vernacexpr.extend_name | Matej Kosik |
| 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 | par: like all: but in parallel | Enrico Tassi |
| 2016-06-16 | Extend Hint Mode to handle the no-head-evar case | Matthieu Sozeau |
| 2016-06-16 | A stronger invariant on the syntax of TacAssert, what allows for a | Hugo Herbelin |
| 2016-06-16 | Merge 'pr/191' into trunk | Enrico Tassi |
| 2016-06-16 | Merge remote-tracking branch 'github/pr/194' into trunk | Maxime Dénès |
| 2016-06-14 | Goal selectors are now tacticals and can be used as such. | Cyprien Mangin |
| 2016-06-14 | Add goal range selectors. | Cyprien Mangin |
| 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-06 | STM: proof block detection/error resilience API | Enrico Tassi |
| 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-02 | Removing pointless field NPatVar. It does not make sense to have Meta | Hugo Herbelin |
| 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 | Removing the Entry module now that rules need not be marshalled. | 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 | In the short term, stronger invariant on the syntax of TacAssert, what | Hugo Herbelin |
| 2016-04-27 | Attempt to slightly improve abusive "Collision between bound | Hugo Herbelin |
| 2016-04-24 | Higher-level API for tactic notations. | Pierre-Marie Pédrot |
| 2016-04-14 | Moving and enhancing the grammar_tactic_prod_item_expr type. | Pierre-Marie Pédrot |
| 2016-04-11 | Removing the ad-hoc tactic_expr type. | Pierre-Marie Pédrot |
| 2016-04-10 | Expliciting the fact that the atomic tactic type is self-contained. | Pierre-Marie Pédrot |
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau |
| 2016-04-01 | Getting rid of the "_mods" parsing entry. | Pierre-Marie Pédrot |
| 2016-03-25 | Moving type_uconstr to Pretyping. | Pierre-Marie Pédrot |
| 2016-03-20 | 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-19 | Moving VernacSolve to an EXTEND-based definition. | Pierre-Marie Pédrot |
