| Commit message (Expand) | Author | Age |
* | Replacing deprecated Implicit Arguments in prelude. | Maxime Dénès | 2016-07-18 |
* | Remove the swap tactic from the prelude. | Maxime Dénès | 2016-07-18 |
* | Fix bug #4923: Warning: appcontext is deprecated. | Pierre-Marie Pédrot | 2016-07-18 |
* | Typo in a comment of stdlib. | Hugo Herbelin | 2016-07-08 |
* | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-07-07 |
|\ |
|
| * | Merge remote-tracking branch 'github/pr/199' into v8.5 | Maxime Dénès | 2016-07-06 |
| |\ |
|
* | | | Fix #4793: Coq 8.6 should accept -compat 8.6 | Maxime Dénès | 2016-07-06 |
| * | | Move option_map notation up | Jason Gross | 2016-07-05 |
| * | | Restore option_map in FMapFacts | Jason Gross | 2016-07-05 |
| | * | Compat84: Don't mess with stdlib modules | Jason Gross | 2016-07-05 |
* | | | Typeclasses: use once in by clause for typeclass eauto | Matthieu Sozeau | 2016-06-28 |
* | | | Add Unset Shrink Abstract/Obligations in Coq85 | Matthieu Sozeau | 2016-06-27 |
* | | | Giving a more natural semantics to injection by default. | Hugo Herbelin | 2016-06-18 |
* | | | Remove unneded hints in NZGcd | Matthieu Sozeau | 2016-06-16 |
* | | | setoid_rewrite: fix the Params resolution tactic | Matthieu Sozeau | 2016-06-16 |
* | | | Typeclasses: stdlib fixes for new search algorithm | Matthieu Sozeau | 2016-06-16 |
* | | | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels. | Hugo Herbelin | 2016-06-16 |
* | | | Adding option "Set Reversible Pattern Implicit" to Specif.v so that an | Hugo Herbelin | 2016-06-16 |
* | | | Changing rule for "*" in Operator_Properties so that, iterated, it | Hugo Herbelin | 2016-06-16 |
| | * | Unbreak singleton list-like notation (-compat 8.4) | Jason Gross | 2016-06-09 |
| |/ |
|
* | | Officially discontinue the experimental coq build via ocamlbuild | Pierre Letouzey | 2016-06-08 |
* | | Relying instead on the Coq85 inclusion! | Hugo Herbelin | 2016-06-06 |
* | | Mode "Bracketing Last Introduction Pattern" is on for 8.4 | Hugo Herbelin | 2016-06-06 |
* | | Mode "Regular Subst Tactic" is on in 8.6. | Hugo Herbelin | 2016-06-06 |
* | | Merge remote-tracking branch 'github/pr/118' into trunk | Maxime Dénès | 2016-06-06 |
|\ \ |
|
* | | | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot | 2016-06-03 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-20 |
|\ \ \
| | |/
| |/| |
|
| * | | Removing unexcepted activation of option "Regular Subst Tactic", since | Hugo Herbelin | 2016-05-14 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-09 |
|\| | |
|
| * | | NPeano : improve compatibility for this deprecated file via compat notations | Pierre Letouzey | 2016-05-04 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-04 |
|\| | |
|
| * | | Int.v: simplify Jason's commit 5b4e3ace | Pierre Letouzey | 2016-05-04 |
| * | | Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int... | Pierre Letouzey | 2016-05-04 |
| |\ \ |
|
* | | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-02 |
|\| | | |
|
* | | | | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it" | 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 "Temporary hack to compensate missing comma while re-printing tactic" | Hugo Herbelin | 2016-04-27 |
* | | | | Temporary hack to compensate missing comma while re-printing tactic | Hugo Herbelin | 2016-04-27 |
* | | | | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels. | Hugo Herbelin | 2016-04-27 |
* | | | | Adding option "Set Reversible Pattern Implicit" to Specif.v so that an | Hugo Herbelin | 2016-04-27 |
* | | | | Changing rule for "*" in Operator_Properties so that, iterated, it | Hugo Herbelin | 2016-04-27 |
| * | | | Fixing bug #4684: Singleton list notation unusable in 8.5pl1. | Pierre-Marie Pédrot | 2016-04-25 |
* | | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-04-09 |
|\| | | |
|
| * | | | Added compatibility coercions from Specif.v which were present in Coq 8.4. | Hugo Herbelin | 2016-04-08 |
| * | | | Add -compat 8.4 econstructor tactics, and tests | Jason Gross | 2016-04-05 |
| * | | | Fix bug #4656 | Jason Gross | 2016-04-05 |
| * | | | Update Coq84.v | Jason Gross | 2016-04-04 |
| * | | | Add compatibility Nonrecursive Elimination Schemes | Jason Gross | 2016-04-04 |
* | | | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau | 2016-04-04 |
|\ \ \ \ |
|