Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-18 |
|\ | |||
| * | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-18 |
| |\ | |||
| | * | Removing output test for module qualification. | Pierre-Marie Pédrot | 2016-10-18 |
| * | | Quick fix to unification regression #4955. | Hugo Herbelin | 2016-10-17 |
| * | | Fixing a few other inconsistencies with notations. | Hugo Herbelin | 2016-10-17 |
| | * | Fixing to #3209 (Not_found due to an occur-check cycle). | Hugo Herbelin | 2016-10-17 |
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-17 |
|\| | | |||
| * | | Fix output test for module qualification. | Pierre-Marie Pédrot | 2016-10-17 |
| * | | Merge PR #300 into v8.6 | Pierre-Marie Pédrot | 2016-10-17 |
| |\ \ | |||
| * | | | Example illustrating non-local inference of the default type of impossible br... | Hugo Herbelin | 2016-10-17 |
| | | * | Merge PR #310 into v8.5 | Pierre-Marie Pédrot | 2016-10-17 |
| | | |\ | |||
| * | | \ | Merge PR #310 into v8.6 | Pierre-Marie Pédrot | 2016-10-17 |
| |\ \ \ \ | | | |_|/ | | |/| | | |||
| | * | | | Test for bug #4874. | Pierre-Marie Pédrot | 2016-10-17 |
| * | | | | Fix bug #5145: Anomaly: index to an anonymous variable. | Pierre-Marie Pédrot | 2016-10-15 |
* | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-12 |
|\| | | | | |||
| * | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-12 |
| |\ \ \ \ | | | |_|/ | | |/| | | |||
| * | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-12 |
| |\ \ \ \ | |||
| | | * | | | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | 2016-10-12 |
| | | * | | | Merge remote-tracking branch 'git/bug5123' into v8.5 | Matthieu Sozeau | 2016-10-12 |
| | |/| | | | |||
| | | * | | | Fix test-suite file 5123 to fail in case of regression | Matthieu Sozeau | 2016-10-11 |
| | | * | | | Fix bug #5123: mark all shelved evars unresolvable | Matthieu Sozeau | 2016-10-11 |
| * | | | | | Reverting generalization and cleaning of the return clause inference in v8.6. | Hugo Herbelin | 2016-10-11 |
| | * | | | | Fix for bug #4863, update the Proofview's env with | Matthieu Sozeau | 2016-10-11 |
| | |/ / / | |||
| | * / / | Add test file for #4416. | Maxime Dénès | 2016-10-10 |
| | |/ / | |||
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-08 |
|\| | | | |||
| * | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-08 |
| |\| | | |||
| * | | | Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq. | Pierre-Marie Pédrot | 2016-10-08 |
| * | | | Fix bug #4464: "Anomaly: variable H' unbound. Please report.". | Pierre-Marie Pédrot | 2016-10-07 |
| | * | | 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.6' | Pierre-Marie Pédrot | 2016-10-05 |
|\| | | | |||
| * | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-05 |
| |\| | | |||
| * | | | Clean up type classes flags and update compat file. | Maxime Dénès | 2016-10-05 |
| | * | | Fixing #4970 (confusion between special "{" and non special "{{" in notations). | Hugo Herbelin | 2016-10-03 |
| * | | | fixing bug 4609: document an option governing the generation of equalities | Yves Bertot | 2016-10-03 |
| * | | | More tests for tactic "subst". | Hugo Herbelin | 2016-10-02 |
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-02 |
|\| | | | |||
| * | | | 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 |
| * | | | test-suite/output-modulo-time made more robust | Enrico Tassi | 2016-09-30 |
| * | | | Merge remote-tracking branch 'github/pr/303' into v8.6 | Maxime Dénès | 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 test-suite. | Maxime Dénès | 2016-09-30 |
| * | | | | | Merge remote-tracking branch 'github/pr/302' into v8.6 | Maxime Dénès | 2016-09-30 |
| |\ \ \ \ \ | |||
| * | | | | | | Restore code ignoring <W> lines in output (camlp5 warnings) | Enrico Tassi | 2016-09-30 |
| * | | | | | | Ignore file names in warning emitted by test-suite/output/* (#5111) | Enrico Tassi | 2016-09-30 |
| * | | | | | | Merge branch 'v8.5' into v8.6 | Maxime Dénès | 2016-09-30 |
| |\ \ \ \ \ \ | | | |/ / / / | | |/| | | | | |||
| | * | | | | | Merge branch '4762' into v8.5 | Maxime Dénès | 2016-09-30 |
| | |\ \ \ \ \ |