aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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.
2018-04-26[ci] Fix another issue with the timing testsJason Gross
There was recently a spurious failure on AppVeyor (I've forgotten which PR). This commit fixes that particular failure.
2018-04-26Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Hugo Herbelin
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-04-22test suite: clean more things (glob, MExtraction.out, distclean aux)Gaëtan Gilbert
NB: I made .aux be cleaned only with distclean imitating the main Makefile.
2018-04-22test suite: print message for failing tests as they comeGaëtan Gilbert
ie you might see make TEST bugs/closed/1337.v TEST bugs/closed/3263.v TEST bugs/closed/7777.v FAILED bugs/closed/3263.v.log TEST bugs/opened/1.v ... report: 3263 failed (should be closed)
2018-04-22test suite Makefile: do not use %.stamp for subsystem targetsGaëtan Gilbert
2018-04-20Fix #6798: coqchk ignores ugraph when comparing constant instancesGaëtan Gilbert
2018-04-16Merge PR #7237: [ssr] fix delayed clears (fix #7045)Maxime Dénès
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
2018-04-13[ssr] fix delayed clears (fix #7045)Enrico Tassi
We take into account all future ipats, not just the ones in the current branch
2018-04-12Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵Jason Gross
removing the test.
2018-04-12Merge PR #500: Move bugs that have been closed on BugzillaMaxime Dénès
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while ↵Emilio Jesus Gallego Arias
looking for a notation for a nested pattern
2018-04-09Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationPierre-Marie Pédrot
2018-04-09Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Maxime Dénès
2018-04-08Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Hugo Herbelin
We ensure that all original names in a spine of matched nested binders are distinct. Note: This enforces that two binders with same internal names are kept disjoint but this does not enforce that we shall respect names exactly as they are printed. Only the original prefix of the internal names are preserved, not their "0" or "1" etc. suffix.
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
We fix it by looking manually for the implementation at each level of nesting rather than using the signature for the n first levels and looking for the implementation only in the n+1-th level.
2018-04-06Fix #5539: algebraic universe produced by cases.Gaëtan Gilbert
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime Dénès
We also make the code of [compact] in kernel/univ.ml a bit clearer.
2018-04-05Improve shell scriptszapashcanon
2018-04-05Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.Théo Zimmermann
Since this is an open bug, it is of lesser importance but non-deterministic tests are a real problem OTOH.
2018-04-04Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Hugo Herbelin
2018-04-04Merge PR #6407: Fix #6404 - Print tactics called by ML tacticsPierre-Marie Pédrot
2018-04-04ssr: check cleared hyps do exist (fix #7050)Enrico Tassi
2018-04-02Update coq_makefile timing testJason Gross
This fixes #5675 (in yet another way). The issue was that `$` (end of string regex) was not properly escaped in `"`s. This handles the issue that is displayed in ``` cat A.v.timing.diff After | Code | Before || Change | % Change --------------------------------------------------------------------------------------------------- 0m01.44s | Total | 0m01.56s || -0m00.12s | -7.92% --------------------------------------------------------------------------------------------------- 0m00.609s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.627s || -0m00.01s | -2.87% 0m00.527s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.552s || -0m00.02s | -4.52% 0m00.304s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.379s || -0m00.07s | -19.78% N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.006s || -0m00.00s | -100.00% 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A --- A.v.timing.diff.desired.processed 2018-03-23 22:22:19.000000000 +0000 +++ A.v.timing.diff.processed 2018-03-23 22:22:19.000000000 +0000 @@ -1,4 +1,4 @@ - N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | N/A + N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | -% ------ ------ After | Code | Before || Change | % Change ``` where, because `Declare Reduction` takes 0.006s rather than 0s, the % change shows up as -100% rather than N/A.
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-04-01Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Pierre-Marie Pédrot
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert
Constrextern.explicitize expected that if implicits were declared they would be declared at least up to the principal argument of the projection, but Context/discharge of implicits does not preserve this. Note the anomaly only happens with primitive projections DISABLED in recent Coqs (>=8.8). Implicit argument experts may consider whether ensuring enough implicits are declared would be better.
2018-03-29Fixes #7110 ("as" untested while looking for notation for nested patterns).Hugo Herbelin
2018-03-29Fix #6770: fixpoint loses locality info in proof mode.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 23:10:20 +0000