| Commit message (Expand) | Author | Age |
* | Bump year in headers. | Maxime Dénès | 2017-06-01 |
* | Revert "Process Next Obligation proofs in parallel (fix #5314)" | Enrico Tassi | 2017-01-21 |
* | Process Next Obligation proofs in parallel (fix #5314) | Enrico Tassi | 2017-01-20 |
* | 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 |
* | Lets Hints/Instances take an optional pattern | Matthieu Sozeau | 2016-11-03 |
* | Complete overhaul of the Arguments vernacular. | Maxime Dénès | 2016-10-27 |
* | Quick fix to #4595 (making notations containing "ltac:" unused for printing). | Hugo Herbelin | 2016-10-04 |
* | 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 |
|/ |
|
* | Support qualified identifiers in Show Match (bug #5050). | Guillaume Melquiond | 2016-08-27 |
* | Add and document match, fix and cofix reduction flags. | Maxime Dénès | 2016-07-01 |
* | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre | 2016-06-27 |
* | COMMENTS: Vernacexpr.extend_name | Matej Kosik | 2016-06-20 |
* | 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-18 |
* | par: like all: but in parallel | Enrico Tassi | 2016-06-17 |
* | 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-16 |
|\ \ |
|
| | * | Goal selectors are now tacticals and can be used as such. | Cyprien Mangin | 2016-06-14 |
| | * | Add goal range selectors. | Cyprien Mangin | 2016-06-14 |
| * | | 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-07 |
| |/ |
|
* / | STM: proof block detection/error resilience API | Enrico Tassi | 2016-06-06 |
|/ |
|
* | 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-03 |
* | Removing pointless field NPatVar. It does not make sense to have Meta | Hugo Herbelin | 2016-06-02 |
* | 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-05-10 |
* | 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-27 |
* | Higher-level API for tactic notations. | Pierre-Marie Pédrot | 2016-04-24 |
* | Moving and enhancing the grammar_tactic_prod_item_expr type. | Pierre-Marie Pédrot | 2016-04-14 |
* | Removing the ad-hoc tactic_expr type. | Pierre-Marie Pédrot | 2016-04-11 |
* | Expliciting the fact that the atomic tactic type is self-contained. | Pierre-Marie Pédrot | 2016-04-10 |
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau | 2016-04-04 |
|\ |
|
* | | Getting rid of the "_mods" parsing entry. | Pierre-Marie Pédrot | 2016-04-01 |
* | | Moving type_uconstr to Pretyping. | Pierre-Marie Pédrot | 2016-03-25 |
* | | 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 |