Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | add test for #7595 | 2018-06-07 | |
| | |||
* | Merge PR #7077: Preserving canonical structure of return predicate in ↵ | 2018-06-05 | |
|\ | | | | | | | vm_compute and native_compute (partial fix to #7068; also fixes #7076)) | ||
* \ | Merge PR #7663: test suite: make target to regenerate failing output tests | 2018-06-05 | |
|\ \ | |||
* | | | Fix #7631: native_compute fails to compile an example in Coq 8.8 | 2018-06-04 | |
| | | | | | | | | | | | | | | | Dependency analysis for separate compilation was not iterated properly on rel_context and named_context. | ||
* | | | Merge PR #7315: An attempt to clarify error message for Arguments needing ↵ | 2018-06-04 | |
|\ \ \ | | | | | | | | | | | | | "rename" flag | ||
| | | * | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate). | 2018-06-04 | |
| |_|/ |/| | | |||
* | | | Merge PR #7229: Deprecate implicit tactic solving. | 2018-06-04 | |
|\ \ \ | |||
| | | * | test suite: make target to regenerate failing output tests | 2018-06-04 | |
| | | | | |||
* | | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵ | 2018-06-04 | |
|\ \ \ \ | | | | | | | | | | | | | | | | pattern-matching names | ||
* \ \ \ \ | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode. | 2018-06-04 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly | 2018-06-04 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7189: Fix #5539: algebraic universe produced by cases. | 2018-06-04 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵ | 2018-06-04 | |
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | tactic unification. | ||
* \ \ \ \ \ \ \ \ | Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵ | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | coinductive types. | ||
* \ \ \ \ \ \ \ \ \ | Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found". | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | | Deprecate implicit tactic solving. | 2018-06-04 | |
| |_|_|_|_|_|_|/ / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel. | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #7578: Allow make clean to work on a fresh clone | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | | Fix #7113: Program Let Fixpoint in section causes anomaly | 2018-05-30 | |
| | | | | | | | | | | | |||
* | | | | | | | | | | | Fix #6951: Unexpected error during scheme creation. | 2018-05-29 | |
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When creating a scheme for bifinite inductive types, we do not create a fixpoint. | ||
* | | | | | | | | | | Add test for #7333: vm_compute segfaults / Anomaly with cofix | 2018-05-29 | |
| | | | | | | | | | | |||
| * | | | | | | | | | Allow make clean to work on a fresh clone | 2018-05-25 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The file `config/Makefile` doesn't exist unless we run `./configure`. We shouldn't have to run `./configure` to run `make clean`. We now no longer error in any case if `config/Makefile` doesn't exist; this is simpler than only not erroring if the target is `clean`. We also now test this property when building on CI. This fixes #7542 | ||
| | | | | | | | | * | An attempt to clarify error message for Arguments needing "rename" flag. | 2018-05-25 | |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Using a formulation which makes it is clear that no renaming has been done. See discussion at issue #2987. | ||
* | | | | | | | | | Fix #7323: coqchk puts polymorphic univs of inductive in global env | 2018-05-24 | |
| | | | | | | | | | |||
* | | | | | | | | | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants | 2018-05-24 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵ | 2018-05-24 | |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | instances | ||
| | | | | * | | | | | | Fix #7586: Anomaly "Uncaught exception Not_found". | 2018-05-23 | |
| |_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The old unification engine was using the unfiltered environment when a context had been cleared, leading to an ill-typed goal. | ||
* | | | | | | | | | | Merge PR #7567: Clean-up dead file in test-suite. | 2018-05-23 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Add test cases from #7554 | 2018-05-20 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Failed in v8.7.2 but were fixed by v8.8.0. | ||
| | | | | * | | | | | Fix #7539: Checker does not properly handle negative coinductive types. | 2018-05-18 | |
| |_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection. | ||
| * | | | | | | | | Clean-up dead file in test-suite. | 2018-05-18 | |
|/ / / / / / / / | |||
* | | | | | | | | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵ | 2018-05-17 | |
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | by default. | ||
| * | | | | | | | | Introduce an option to allow nested lemma, and turn it off by default. | 2018-05-17 | |
| | | | | | | | | | |||
* | | | | | | | | | Modify make system to include Makefile.common in the test suite | 2018-05-16 | |
| | | | | | | | | | |||
* | | | | | | | | | unit tests: add .merlin | 2018-05-16 | |
| | | | | | | | | | |||
* | | | | | | | | | add unit tests to test suite | 2018-05-16 | |
|/ / / / / / / / | |||
* | | | | | | | | Merge PR #7484: Fix non-portable shebang in test-suite. | 2018-05-16 | |
|\ \ \ \ \ \ \ \ | |||
* | | | | | | | | | [ssr] import ssreflect test suite from math-comp | 2018-05-15 | |
| | | | | | | | | | |||
* | | | | | | | | | Merge PR #7502: Fixing little printing bug with "Locate" on recursive notations | 2018-05-14 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵ | 2018-05-14 | |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | symlink from repo | ||
| | * | | | | | | | | | Fixing a bug in printing the body of a located notation. | 2018-05-13 | |
| |/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was introduced between v8.5 and v8.6 (presumably 63f3ca8). | ||
| * | | | | | | | | | Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo | 2018-05-13 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #7065 | ||
* | | | | | | | | | | Merge PR #7477: Support for notations with autonomous only-parsing and ↵ | 2018-05-13 | |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | only-printing declarations. | ||
| | | | | | * | | | | | Fix #4403: insufficient handling of type-in-type in kernel. | 2018-05-13 | |
| |_|_|_|_|/ / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #7470: use at least 6 Xs in mktemp filename templates | 2018-05-11 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | Fix non-portable shebang in test-suite. | 2018-05-11 | |
| |_|_|/ / / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #7363: [ci] Fix another issue with the timing tests | 2018-05-11 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | Fixes #7462, part 2 (only-printing not make believe parsing rule is declared). | 2018-05-10 | |
| | | | | | | | | | | | |||
| | | * | | | | | | | | Fixes part 1 of #7462 (only-printing not to override existing interp rule). | 2018-05-10 | |
| | | |/ / / / / / / | |||
| | * / / / / / / / | use at least 6 Xs in mktemp filename templates | 2018-05-09 | |
| | |/ / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | OpenBSD mktemp fails with an error otherwise. |