aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)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 ↵Matthieu Sozeau
pattern-matching names
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 ↵Matthieu Sozeau
tactic unification.
2018-06-04Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵Matthieu Sozeau
coinductive types.
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
When creating a scheme for bifinite inductive types, we do not create a fixpoint.
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
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
2018-05-25An attempt to clarify error message for Arguments needing "rename" flag.Hugo Herbelin
Using a formulation which makes it is clear that no renaming has been done. See discussion at issue #2987.
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 ↵Pierre-Marie Pédrot
instances
2018-05-23Fix #7586: Anomaly "Uncaught exception Not_found".Pierre-Marie Pédrot
The old unification engine was using the unfiltered environment when a context had been cleared, leading to an ill-typed goal.
2018-05-23Merge PR #7567: Clean-up dead file in test-suite.Enrico Tassi
2018-05-20Add test cases from #7554Tej Chajed
Failed in v8.7.2 but were fixed by v8.8.0.
2018-05-18Fix #7539: Checker does not properly handle negative coinductive types.Pierre-Marie Pédrot
The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection.
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 ↵Emilio Jesus Gallego Arias
by default.
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 ↵Gaëtan Gilbert
symlink from repo
2018-05-13Fixing a bug in printing the body of a located notation.Hugo Herbelin
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
Fixes #7065
2018-05-13Merge PR #7477: Support for notations with autonomous only-parsing and ↵Emilio Jesus Gallego Arias
only-printing declarations.
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
OpenBSD mktemp fails with an error otherwise.
2018-05-09test for coqc -oEnrico Tassi
2018-05-03Merge PR #7134: When an error comes from loading the prelude, tell it ↵Emilio Jesus Gallego Arias
happened at initialization time
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase.
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:00:32 +0000