aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
...
* | | Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...Gravatar Maxime Dénès2018-06-05
|\ \ \
* \ \ \ Merge PR #7663: test suite: make target to regenerate failing output testsGravatar Enrico Tassi2018-06-05
|\ \ \ \
* | | | | Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Maxime Dénès2018-06-04
* | | | | Merge PR #7315: An attempt to clarify error message for Arguments needing "re...Gravatar Maxime Dénès2018-06-04
|\ \ \ \ \
| | | * | | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).Gravatar Hugo Herbelin2018-06-04
| |_|/ / / |/| | | |
* | | | | Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\ \ \ \ \
| | | * | | test suite: make target to regenerate failing output testsGravatar Gaëtan Gilbert2018-06-04
* | | | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7189: Fix #5539: algebraic universe produced by cases.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Maxime Dénès2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7578: Allow make clean to work on a fresh cloneGravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | | | Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Gaëtan Gilbert2018-05-30
* | | | | | | | | | | | | Fix #6951: Unexpected error during scheme creation.Gravatar Pierre-Marie Pédrot2018-05-29
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Add test for #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-29
| * | | | | | | | | | | Allow make clean to work on a fresh cloneGravatar Jason Gross2018-05-25
| | | | | | | | | * | | An attempt to clarify error message for Arguments needing "rename" flag.Gravatar Hugo Herbelin2018-05-25
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
* | | | | | | | | | | Fix #7323: coqchk puts polymorphic univs of inductive in global envGravatar Gaëtan Gilbert2018-05-24
* | | | | | | | | | | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsGravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | | Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Pierre-Marie Pédrot2018-05-23
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7567: Clean-up dead file in test-suite.Gravatar Enrico Tassi2018-05-23
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Add test cases from #7554Gravatar Tej Chajed2018-05-20
| | | | | * | | | | | | Fix #7539: Checker does not properly handle negative coinductive types.Gravatar Pierre-Marie Pédrot2018-05-18
| |_|_|_|/ / / / / / / |/| | | | | | | | | |
| * | | | | | | | | | Clean-up dead file in test-suite.Gravatar Théo Zimmermann2018-05-18
|/ / / / / / / / / /
* | | | | | | | | | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...Gravatar Emilio Jesus Gallego Arias2018-05-17
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
* | | | | | | | | | | Modify make system to include Makefile.common in the test suiteGravatar Gaëtan Gilbert2018-05-16
* | | | | | | | | | | unit tests: add .merlinGravatar Gaëtan Gilbert2018-05-16
* | | | | | | | | | | add unit tests to test suiteGravatar Paul Steckler2018-05-16
|/ / / / / / / / / /
* | | | | | | | | | Merge PR #7484: Fix non-portable shebang in test-suite.Gravatar Enrico Tassi2018-05-16
|\ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | [ssr] import ssreflect test suite from math-compGravatar Enrico Tassi2018-05-15
* | | | | | | | | | | Merge PR #7502: Fixing little printing bug with "Locate" on recursive notationsGravatar Emilio Jesus Gallego Arias2018-05-14
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...Gravatar Gaëtan Gilbert2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | Fixing a bug in printing the body of a located notation.Gravatar Hugo Herbelin2018-05-13
| |/ / / / / / / / / / / |/| | | | | | | | | | |
| * | | | | | | | | | | Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoGravatar Ralf Jung2018-05-13
* | | | | | | | | | | | Merge PR #7477: Support for notations with autonomous only-parsing and only-p...Gravatar Emilio Jesus Gallego Arias2018-05-13
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | | Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Gaëtan Gilbert2018-05-13
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7470: use at least 6 Xs in mktemp filename templatesGravatar Gaëtan Gilbert2018-05-11
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | | | Fix non-portable shebang in test-suite.Gravatar Théo Zimmermann2018-05-11
| |_|_|/ / / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7363: [ci] Fix another issue with the timing testsGravatar Gaëtan Gilbert2018-05-11
|\ \ \ \ \ \ \ \ \ \ \ \
| | | * | | | | | | | | | Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
| | | * | | | | | | | | | Fixes part 1 of #7462 (only-printing not to override existing interp rule).Gravatar Hugo Herbelin2018-05-10
| | | |/ / / / / / / / /
| | * / / / / / / / / / use at least 6 Xs in mktemp filename templatesGravatar Sven M. Hallberg2018-05-09
| | |/ / / / / / / / /
* | / / / / / / / / / test for coqc -oGravatar Enrico Tassi2018-05-09
| |/ / / / / / / / / |/| | | | | | | | |