Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | | | 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 | |
| | |\ \ \ \ \ \ | ||||
| | | * | | | | | | Fix #4762. | Cyprien Mangin | 2016-09-30 | |
| | | | | | * | | | LtacProf cutoff is for total percent, not time | Jason Gross | 2016-09-29 | |
| | |_|_|_|/ / / | |/| | | | | | | ||||
| | | | * | | | | Set the default LtacProf cutoff to 2% | Jason Gross | 2016-09-29 | |
| | |_|/ / / / | |/| | | | | | ||||
| | | | | * | | 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 #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 a bug in subst releaved by an OCaml warning. | Maxime Dénès | 2016-09-29 | |
| | | | |/ / | ||||
| * | | | | | test-suite: fix sed on OS X, does not handle + | Matthieu Sozeau | 2016-09-29 | |
| * | | | | | Argument : assert does fail if no arg is given (fix #4864) | Enrico Tassi | 2016-09-29 | |
| | |/ / / | |/| | | | ||||
| | * | | | Fix bug #4723 and FIXME in API for solve_by_tac | Matthieu Sozeau | 2016-09-28 | |
| |/ / / | ||||
| * | | | Typeclass backtracking example by J. Leivant | 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 | |
* | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 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 | |
| * | | | | Posssible abstractions over goal variables when inferring match return clause. | Hugo Herbelin | 2016-09-26 | |
| * | | | | Trying an abstracting dependencies heuristic for the match return clause even... | Hugo Herbelin | 2016-09-26 | |
| * | | | | Trying a no-inversion no-dependency heuristic for match return clause. | Hugo Herbelin | 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.6' | Pierre-Marie Pédrot | 2016-09-23 | |
|\| | | | | ||||
| * | | | | 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 | |
* | | | | | Fixing test FunExt.v. | Hugo Herbelin | 2016-09-19 | |
* | | | | | extensionality: Handle dependently-used hypotheses | Jason Gross | 2016-09-19 | |
* | | | | | Adding an "extensionality in H" tactic which applies functional | Hugo Herbelin | 2016-09-19 | |
| * | | | | Further "decide equality" tests on demand of Jason. | Hugo Herbelin | 2016-09-17 | |
| * | | | | Added a test file for contradiction. | Hugo Herbelin | 2016-09-15 | |
| * | | | | Continuing fix to #5078, taking also into account intropatterns. | Hugo Herbelin | 2016-09-15 | |
* | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-14 | |
|\| | | | | ||||
| * | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-14 | |
| |\| | | | ||||
| | * | | | Fixing test-suite after commit 43104a0b. | Pierre-Marie Pédrot | 2016-09-14 | |
| * | | | | test-suite/output-modulo-time made more robust | Enrico Tassi | 2016-09-13 | |
| | * | | | Fixing a recursive notation bug raised on coq-club on Sep 12, 2016. | Hugo Herbelin | 2016-09-12 | |
| * | | | | Merge remote-tracking branch 'github-coq/pr/249' into v8.6 | Matthieu Sozeau | 2016-09-12 | |
| |\ \ \ \ | ||||
| * | | | | | Add support for testing output mod timing changes | Jason Gross | 2016-09-11 | |
| * | | | | | 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 |