Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge branch 'v8.6' | 2017-07-04 | |
|\ | |||
* | | Bump year in headers. | 2017-07-04 | |
* | | Merge PR#843: closing bug #5618 introduce by PR 828 | 2017-06-30 | |
|\ \ | |||
| * | | closing bug #5618 introduce by PR 828 | 2017-06-29 | |
* | | | Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails with... | 2017-06-27 | |
|\ \ \ | |||
* \ \ \ | Merge PR#826: Put plugin exports in the right compatibility file | 2017-06-26 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#828: closing bug #4250 | 2017-06-26 | |
|\ \ \ \ \ | | |_|/ / | |/| | | | |||
* | | | | | Merge PR#794: Cleanup of ltac cmxs | 2017-06-23 | |
|\ \ \ \ \ | |||
| | * | | | | closing bug #4250 | 2017-06-23 | |
| |/ / / / |/| | | | | |||
| | | | * | Add tests for handling of warnings | 2017-06-23 | |
| | * | | | Add test-suite file for funind, extraction with compat 8.6 | 2017-06-22 | |
| |/ / / |/| | | | |||
| | * | | Should fix a false negative reported by deps-order.sh. | 2017-06-21 | |
| |/ / |/| | | |||
* | | | Merge PR#807: romega: fix a slowdown | 2017-06-20 | |
|\ \ \ | |||
* \ \ \ | Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological | 2017-06-19 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#760: Fixing base_include after loc is an option + a better test that... | 2017-06-19 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#613: Cumulativity for inductive types | 2017-06-19 | |
|\ \ \ \ \ \ | |||
* | | | | | | | Test case for bug 5578. | 2017-06-19 | |
| | | | * | | | romega: avoid potential slowdown when changing concl by reified version | 2017-06-16 | |
* | | | | | | | Increase the time limit on 4366.v to make gitlab work better. | 2017-06-16 | |
| |_|_|/ / / |/| | | | | | |||
| * | | | | | Fix a bug in cumulativity | 2017-06-16 | |
| * | | | | | Clean up universes of constants and inductives | 2017-06-16 | |
| * | | | | | Move (part of) tests from checker to success | 2017-06-16 | |
| * | | | | | Checker add test for non-trivial constraints | 2017-06-16 | |
| * | | | | | Change the option to Set Inductive Cumulativity | 2017-06-16 | |
| * | | | | | Correct coqchk reduction | 2017-06-16 | |
| * | | | | | Disable debug printing | 2017-06-16 | |
| * | | | | | Fix bugs and add an option for cumulativity | 2017-06-16 | |
| * | | | | | Fix bugs | 2017-06-16 | |
|/ / / / / | |||
| | | | * | Merge PR#713: Bump year in headers. | 2017-06-15 | |
| | | | |\ | |||
| | | | * \ | Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints | 2017-06-15 | |
| | | | |\ \ | |||
| | | | * \ \ | Merge PR#752: Adding a test case as requested in bug 5205. | 2017-06-15 | |
| | | | |\ \ \ | |||
| | | | * \ \ \ | Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module imports | 2017-06-15 | |
| | | | |\ \ \ \ | |||
* | | | | \ \ \ \ | Merge PR#719: Constrexpr.Numeral without bigint | 2017-06-15 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | plugins/ltac : avoid spurious .cmxs files | 2017-06-15 | |
* | | | | | | | | | | Merge PR#375: Deprecation | 2017-06-15 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | Remove dependency on -compat flag in coq_makefile test suite. | 2017-06-15 | |
| |_|_|_|/ / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match"). | 2017-06-14 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | [typeclasses eauto] Fix bug #3943: non-termination in topological | 2017-06-14 | |
* | | | | | | | | | | | Prelude : no more autoload of plugins extraction and recdef | 2017-06-14 | |
| | | * | | | | | | | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t) | 2017-06-14 | |
| |_|/ / / / / / / / |/| | | | | | | | | | |||
| | * | | | | | | | | Remove support for Coq 8.4. | 2017-06-14 | |
| |/ / / / / / / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR#498: Bignums as a separate opam package | 2017-06-14 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR#385: Equality of sigma types | 2017-06-13 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR#757: Better sectioning on travis log printing in test-suite | 2017-06-13 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | 2017-06-13 | |
| |_|/ / / / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR#709: Bytecode compilation apart from 'make world', again | 2017-06-12 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | Add support for "-bypass-API" argument of "coq_makefile" | 2017-06-12 | |
* | | | | | | | | | | | make test-suite/save-logs.sh usable also on old MacOS X | 2017-06-12 | |
| | | | | * | | | | | | A stronger test that #use"include";; works well. | 2017-06-11 | |
| |_|_|_|/ / / / / / |/| | | | | | | | | | |||
| | * | | | | | | | | Fix Travis sectioning | 2017-06-10 |