| Commit message (Expand) | Author | Age |
... | |
| * | | | | evarconv.ml: Fix bug #4529, primproj unfolding | Matthieu Sozeau | 2016-10-06 |
| * | | | | unification.ml: fix for bug #4763, unif regression | Matthieu Sozeau | 2016-10-06 |
* | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-05 |
|\| | | | |
|
| * | | | | Fixing #4970 (confusion between special "{" and non special "{{" in notations). | Hugo Herbelin | 2016-10-03 |
* | | | | | Fix bug #4661: Cannot mask the absolute name. | Pierre-Marie Pédrot | 2016-10-01 |
* | | | | | Fix bug #5045: [generalize] creates ill-typed terms in 8.6. | Pierre-Marie Pédrot | 2016-09-30 |
* | | | | | Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk. | Pierre-Marie Pédrot | 2016-09-30 |
* | | | | | Merge remote-tracking branch 'github/pr/299' into v8.6 | Maxime Dénès | 2016-09-30 |
|\ \ \ \ \ |
|
* \ \ \ \ \ | Merge branch 'v8.5' into v8.6 | Maxime Dénès | 2016-09-30 |
|\ \ \ \ \ \
| | |/ / / /
| |/| | | | |
|
| * | | | | | Fix #4762. | Cyprien Mangin | 2016-09-30 |
| | | * | | | Move vector/list compat notations to their relevant files | Jason Gross | 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 |
* | | | | | Merge branch 'bug5036' into v8.6 | Matthieu Sozeau | 2016-09-29 |
|\ \ \ \ \ |
|
| * | | | | | Fix bug #5036 autorewrite, sections and universes | Matthieu Sozeau | 2016-09-29 |
* | | | | | | Merge branch 'bug4723' into v8.6 | Matthieu Sozeau | 2016-09-29 |
|\ \ \ \ \ \ |
|
| | | | | | * | Fix bug 4969, autoapply was not tagging shelved subgoals correctly as unresol... | Matthieu Sozeau | 2016-09-29 |
| | | |_|_|/
| | |/| | | |
|
| | | | * | | Fix bug #4869, allow Prop, Set, and level names in constraints. | Matthieu Sozeau | 2016-09-29 |
| | | |/ /
| | |/| | |
|
* | / | | | Fix bug #5011: Anomaly on [Existing Class]. | Pierre-Marie Pédrot | 2016-09-29 |
| |/ / /
|/| | | |
|
| * | | | Fix bug #4723 and FIXME in API for solve_by_tac | Matthieu Sozeau | 2016-09-28 |
|/ / / |
|
* | | | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès | 2016-09-28 |
|\ \ \ |
|
* | | | | Add fixed test-suite file for bug #4527 | Matthieu Sozeau | 2016-09-27 |
* | | | | Unbreak Ltac [ | .. | ] notation in -compat 8.5 | Jason Gross | 2016-09-26 |
* | | | | Fix bug #4785 (use [ ] for vector nil) | Jason Gross | 2016-09-26 |
* | | | | Fix bug #5093: typeclasses eauto depth arg does not accept a var. | Pierre-Marie Pédrot | 2016-09-26 |
* | | | | Adding a test for bug #5096. | Pierre-Marie Pédrot | 2016-09-24 |
* | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-23 |
|\ \ \ \
| | |/ /
| |/| | |
|
| * | | | Fixing #5095 (non relevant too strict test in let-in abstraction). | Hugo Herbelin | 2016-09-22 |
* | | | | Continuing fix to #5078, taking also into account intropatterns. | Hugo Herbelin | 2016-09-15 |
* | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-14 |
|\| | | |
|
* | | | | Merge remote-tracking branch 'github-coq/pr/249' into v8.6 | Matthieu Sozeau | 2016-09-12 |
|\ \ \ \ |
|
* | | | | | Add a test for 4836 | Jason Gross | 2016-09-11 |
| | * | | | Test for #5077. | Hugo Herbelin | 2016-09-10 |
| * | | | | no-refold patch | Paul Steckler | 2016-09-09 |
|/ / / / |
|
* | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-07 |
|\| | | |
|
| * | | | Test file for #5065 - Anomaly: Not a proof by induction | Maxime Dénès | 2016-09-05 |
* | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-02 |
|\| | | |
|
| * | | | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot | 2016-08-31 |
* | | | | Fix bug #4893: not_evar: unexpected failure in 8.5pl1. | Pierre-Marie Pédrot | 2016-08-30 |
* | | | | Fix bug #3920: eapply masks an hypothesis name. | Pierre-Marie Pédrot | 2016-08-30 |
* | | | | Fix bug #4764: Syntactic notation externalization breaks. | Pierre-Marie Pédrot | 2016-08-28 |
* | | | | Fix bug #4904: [Import] does not load intermediately unqualified names of ali... | Pierre-Marie Pédrot | 2016-08-23 |
* | | | | Test file for bug #4187. | Pierre-Marie Pédrot | 2016-08-19 |
* | | | | Adding a test for bug #4653. | Pierre-Marie Pédrot | 2016-08-18 |
* | | | | Fixing #3070 ("subst" taking properly into account chains of dependencies). | Hugo Herbelin | 2016-08-17 |
* | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-08-16 |
|\| | | |
|
| * | | | Fix bug #4673: regression in setoid_rewrite. | Matthieu Sozeau | 2016-07-29 |
* | | | | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | 2016-07-29 |
|\| | | |
|
| * | | | Fix bug #3886, generation of obligations of fixes | Matthieu Sozeau | 2016-07-29 |
| * | | | Fix #4769, univ poly and elim schemes in sections | Matthieu Sozeau | 2016-07-29 |