Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | Merge PR #7077: Preserving canonical structure of return predicate in ↵ | Maxime Dénès | 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 | Enrico Tassi | 2018-06-05 | |
|\ \ \ \ | ||||
* | | | | | Fix #7631: native_compute fails to compile an example in Coq 8.8 | Maxime Dénès | 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 ↵ | Maxime Dénès | 2018-06-04 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | "rename" flag | |||
| | | * | | | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate). | Hugo Herbelin | 2018-06-04 | |
| |_|/ / / |/| | | | | ||||
* | | | | | Merge PR #7229: Deprecate implicit tactic solving. | Hugo Herbelin | 2018-06-04 | |
|\ \ \ \ \ | ||||
| | | * | | | test suite: make target to regenerate failing output tests | Gaëtan Gilbert | 2018-06-04 | |
| | | | | | | ||||
* | | | | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵ | Matthieu Sozeau | 2018-06-04 | |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | pattern-matching names | |||
* \ \ \ \ \ \ | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode. | Matthieu Sozeau | 2018-06-04 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly | Matthieu Sozeau | 2018-06-04 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #7189: Fix #5539: algebraic universe produced by cases. | Matthieu Sozeau | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵ | Matthieu Sozeau | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tactic unification. | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵ | Matthieu Sozeau | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | coinductive types. | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found". | Matthieu Sozeau | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | | Deprecate implicit tactic solving. | Pierre-Marie Pédrot | 2018-06-04 | |
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel. | Maxime Dénès | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR #7578: Allow make clean to work on a fresh clone | Enrico Tassi | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | Fix #7113: Program Let Fixpoint in section causes anomaly | Gaëtan Gilbert | 2018-05-30 | |
| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | Fix #6951: Unexpected error during scheme creation. | Pierre-Marie Pédrot | 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 | Maxime Dénès | 2018-05-29 | |
| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | Allow make clean to work on a fresh clone | Jason Gross | 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. | Hugo Herbelin | 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 | Gaëtan Gilbert | 2018-05-24 | |
| | | | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants | Pierre-Marie Pédrot | 2018-05-24 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵ | Pierre-Marie Pédrot | 2018-05-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | instances | |||
| | | | | * | | | | | | | | Fix #7586: Anomaly "Uncaught exception Not_found". | Pierre-Marie Pédrot | 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. | Enrico Tassi | 2018-05-23 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Add test cases from #7554 | Tej Chajed | 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. | Pierre-Marie Pédrot | 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. | Théo Zimmermann | 2018-05-18 | |
|/ / / / / / / / / / | ||||
* | | | | | | | | | | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵ | Emilio Jesus Gallego Arias | 2018-05-17 | |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | by default. | |||
| * | | | | | | | | | | Introduce an option to allow nested lemma, and turn it off by default. | Théo Zimmermann | 2018-05-17 | |
| | | | | | | | | | | | ||||
* | | | | | | | | | | | Modify make system to include Makefile.common in the test suite | Gaëtan Gilbert | 2018-05-16 | |
| | | | | | | | | | | | ||||
* | | | | | | | | | | | unit tests: add .merlin | Gaëtan Gilbert | 2018-05-16 | |
| | | | | | | | | | | | ||||
* | | | | | | | | | | | add unit tests to test suite | Paul Steckler | 2018-05-16 | |
|/ / / / / / / / / / | ||||
* | | | | | | | | | | Merge PR #7484: Fix non-portable shebang in test-suite. | Enrico Tassi | 2018-05-16 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | | [ssr] import ssreflect test suite from math-comp | Enrico Tassi | 2018-05-15 | |
| | | | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR #7502: Fixing little printing bug with "Locate" on recursive notations | Emilio Jesus Gallego Arias | 2018-05-14 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵ | Gaëtan Gilbert | 2018-05-14 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | symlink from repo | |||
| | * | | | | | | | | | | | Fixing a bug in printing the body of a located notation. | Hugo Herbelin | 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 | Ralf Jung | 2018-05-13 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #7065 | |||
* | | | | | | | | | | | | Merge PR #7477: Support for notations with autonomous only-parsing and ↵ | Emilio Jesus Gallego Arias | 2018-05-13 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | only-printing declarations. | |||
| | | | | | * | | | | | | | Fix #4403: insufficient handling of type-in-type in kernel. | Gaëtan Gilbert | 2018-05-13 | |
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR #7470: use at least 6 Xs in mktemp filename templates | Gaëtan Gilbert | 2018-05-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | * | | | | | | | | | Fix non-portable shebang in test-suite. | Théo Zimmermann | 2018-05-11 | |
| |_|_|/ / / / / / / / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR #7363: [ci] Fix another issue with the timing tests | Gaëtan Gilbert | 2018-05-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | | Fixes #7462, part 2 (only-printing not make believe parsing rule is declared). | Hugo Herbelin | 2018-05-10 | |
| | | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | Fixes part 1 of #7462 (only-printing not to override existing interp rule). | Hugo Herbelin | 2018-05-10 | |
| | | |/ / / / / / / / / | ||||
| | * / / / / / / / / / | use at least 6 Xs in mktemp filename templates | Sven M. Hallberg | 2018-05-09 | |
| | |/ / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | OpenBSD mktemp fails with an error otherwise. | |||
* | / / / / / / / / / | test for coqc -o | Enrico Tassi | 2018-05-09 | |
| |/ / / / / / / / / |/| | | | | | | | | |