aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-06-04Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).Hugo Herbelin
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04test suite: make target to regenerate failing output testsGaëtan Gilbert
2018-06-04Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...Matthieu Sozeau
2018-06-04Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Matthieu Sozeau
2018-06-04Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyMatthieu Sozeau
2018-06-04Merge PR #7189: Fix #5539: algebraic universe produced by cases.Matthieu Sozeau
2018-06-04Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...Matthieu Sozeau
2018-06-04Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Matthieu Sozeau
2018-06-04Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Matthieu Sozeau
2018-06-04Deprecate implicit tactic solving.Pierre-Marie Pédrot
2018-06-04Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Maxime Dénès
2018-05-31Merge PR #7578: Allow make clean to work on a fresh cloneEnrico Tassi
2018-05-30Fix #7113: Program Let Fixpoint in section causes anomalyGaëtan Gilbert
2018-05-29Fix #6951: Unexpected error during scheme creation.Pierre-Marie Pédrot
2018-05-29Add test for #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-25Allow make clean to work on a fresh cloneJason Gross
2018-05-25An attempt to clarify error message for Arguments needing "rename" flag.Hugo Herbelin
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-05-24Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsPierre-Marie Pédrot
2018-05-24Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...Pierre-Marie Pédrot
2018-05-23Fix #7586: Anomaly "Uncaught exception Not_found".Pierre-Marie Pédrot
2018-05-23Merge PR #7567: Clean-up dead file in test-suite.Enrico Tassi
2018-05-20Add test cases from #7554Tej Chajed
2018-05-18Fix #7539: Checker does not properly handle negative coinductive types.Pierre-Marie Pédrot
2018-05-18Clean-up dead file in test-suite.Théo Zimmermann
2018-05-17Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...Emilio Jesus Gallego Arias
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-16Modify make system to include Makefile.common in the test suiteGaëtan Gilbert
2018-05-16unit tests: add .merlinGaëtan Gilbert
2018-05-16add unit tests to test suitePaul Steckler
2018-05-16Merge PR #7484: Fix non-portable shebang in test-suite.Enrico Tassi
2018-05-15[ssr] import ssreflect test suite from math-compEnrico Tassi
2018-05-14Merge PR #7502: Fixing little printing bug with "Locate" on recursive notationsEmilio Jesus Gallego Arias
2018-05-14Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...Gaëtan Gilbert
2018-05-13Fixing a bug in printing the body of a located notation.Hugo Herbelin
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
2018-05-13Merge PR #7477: Support for notations with autonomous only-parsing and only-p...Emilio Jesus Gallego Arias
2018-05-13Fix #4403: insufficient handling of type-in-type in kernel.Gaëtan Gilbert
2018-05-11Merge PR #7470: use at least 6 Xs in mktemp filename templatesGaëtan Gilbert
2018-05-11Fix non-portable shebang in test-suite.Théo Zimmermann
2018-05-11Merge PR #7363: [ci] Fix another issue with the timing testsGaëtan Gilbert
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-05-10Fixes part 1 of #7462 (only-printing not to override existing interp rule).Hugo Herbelin
2018-05-09use at least 6 Xs in mktemp filename templatesSven M. Hallberg
2018-05-09test for coqc -oEnrico Tassi
2018-05-03Merge PR #7134: When an error comes from loading the prelude, tell it happene...Emilio Jesus Gallego Arias
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:28:04 +0000