aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
...
* | | | | | | | | test for coqc -oGravatar Enrico Tassi2018-05-09
| |/ / / / / / / |/| | | | | | |
* | | | | | | | Merge PR #7134: When an error comes from loading the prelude, tell it ↵Gravatar Emilio Jesus Gallego Arias2018-05-03
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | happened at initialization time
| * | | | | | | | Making explicit that errors happen in one of five executation phases.Gravatar Hugo Herbelin2018-05-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | Make "intro"/"intros" progress on existential variables.Gravatar Hugo Herbelin2018-05-02
|/ / / / / / / /
* | | | | | | | Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | | | [ci] Fix another issue with the timing testsGravatar Jason Gross2018-04-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was recently a spurious failure on AppVeyor (I've forgotten which PR). This commit fixes that particular failure.
* | | | | | | | Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Gravatar Hugo Herbelin2018-04-26
|/ / / / / / /
| | * / / / / Fix #7327: coqchk subtyping of polymorphic constantsGravatar Gaëtan Gilbert2018-04-23
| |/ / / / /
* | | | | | test suite: clean more things (glob, MExtraction.out, distclean aux)Gravatar Gaëtan Gilbert2018-04-22
| | | | | | | | | | | | | | | | | | | | | | | | NB: I made .aux be cleaned only with distclean imitating the main Makefile.
* | | | | | test suite: print message for failing tests as they comeGravatar Gaëtan Gilbert2018-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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)
* | | | | | test suite Makefile: do not use %.stamp for subsystem targetsGravatar Gaëtan Gilbert2018-04-22
| | | | | |
| * | | | | Fix #6798: coqchk ignores ugraph when comparing constant instancesGravatar Gaëtan Gilbert2018-04-20
|/ / / / /
* | | | | Merge PR #7237: [ssr] fix delayed clears (fix #7045)Gravatar Maxime Dénès2018-04-16
|\ \ \ \ \
* | | | | | [ltac] Deprecate nameless fix/cofix.Gravatar Emilio Jesus Gallego Arias2018-04-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | [ssr] fix delayed clears (fix #7045)Gravatar Enrico Tassi2018-04-13
|/ / / / / | | | | | | | | | | | | | | | | | | | | We take into account all future ipats, not just the ones in the current branch
* | | | | Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵Gravatar Jason Gross2018-04-12
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | removing the test.
* \ \ \ \ \ Merge PR #500: Move bugs that have been closed on BugzillaGravatar Maxime Dénès2018-04-12
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7087: Congruence tactic engine updateGravatar Pierre-Marie Pédrot2018-04-12
|\ \ \ \ \ \ \
| | * | | | | | Fix the status of some resolved bugsGravatar Tej Chajed2018-04-11
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while ↵Gravatar Emilio Jesus Gallego Arias2018-04-09
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | looking for a notation for a nested pattern
* \ \ \ \ \ \ \ Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationGravatar Pierre-Marie Pédrot2018-04-09
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Gravatar Maxime Dénès2018-04-09
|\ \ \ \ \ \ \ \ \
| | | | | | | | | * Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Gravatar Hugo Herbelin2018-04-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | * | | Fix #5539: algebraic universe produced by cases.Gravatar Gaëtan Gilbert2018-04-06
| | | | | | | | |/ | | | | | | | |/|
| | * | | | | | | Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We also make the code of [compact] in kernel/univ.ml a bit clearer.
* | | | | | | | | Improve shell scriptsGravatar zapashcanon2018-04-05
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | * | | Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.Gravatar Théo Zimmermann2018-04-05
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | Since this is an open bug, it is of lesser importance but non-deterministic tests are a real problem OTOH.
* | | | | | | Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Gravatar Hugo Herbelin2018-04-04
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | |
* | | | | | | Merge PR #6407: Fix #6404 - Print tactics called by ML tacticsGravatar Pierre-Marie Pédrot2018-04-04
|\ \ \ \ \ \ \
| | | * | | | | ssr: check cleared hyps do exist (fix #7050)Gravatar Enrico Tassi2018-04-04
| |_|/ / / / / |/| | | | | |
* | | | | | | Update coq_makefile timing testGravatar Jason Gross2018-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | | Fix #6404 - Print tactics called by ML tacticsGravatar Jason Gross2018-04-02
|/ / / / / /
* | | | | | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Gravatar Pierre-Marie Pédrot2018-04-01
|\ \ \ \ \ \
* | | | | | | Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
| | | | | | |
| | * | | | | Fix #6257: anomaly with Printing Projections and Context.Gravatar Gaëtan Gilbert2018-03-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | Fixes #7110 ("as" untested while looking for notation for nested patterns).Gravatar Hugo Herbelin2018-03-29
| | | | | | |
| | | | | | * Fix #6770: fixpoint loses locality info in proof mode.Gravatar Gaëtan Gilbert2018-03-29
| | | | | | |
* | | | | | | Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Gravatar Pierre-Marie Pédrot2018-03-29
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use a lower level function that accesses the proof without raising an anomaly. This is a direct candidate for backport, so I used a V82 API but eventually this API should be cleaned up.
| * | | | | Supporting fix/cofix in Ltac pattern-matching (wish #7092).Gravatar Hugo Herbelin2018-03-28
| |/ / / / | | | | | | | | | | | | | | | | | | | | This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern.
* | | | | Merge PR #7090: stm: don't propagate side effects when editing a proofGravatar Emilio Jesus Gallego Arias2018-03-28
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6961: [test-suite] Add backtracking test for `Load`.Gravatar Enrico Tassi2018-03-28
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| | * | | | stm: don't propagate side effects when editing a proofGravatar Enrico Tassi2018-03-27
| | |/ / /
| | | * / Congruence: Fixing a bug with native projections.Gravatar Hugo Herbelin2018-03-27
| | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There is a code to turn constants denoting projections into proper primitive projections, but it did not drop parameters. The code seems anyway redundant with an "expand_projections" which is already present in Cctac.decompose_term. After removal of this code, the two calls to congruence added to cc.v work.
| | | * Fixes #7011 (Fix/CoFix were not considered in tactic unification).Gravatar Hugo Herbelin2018-03-26
| | |/
* | / Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
| |/ |/| | | | | For instance, error in "Goal forall a f, f a = 0" is now located.
| * [test-suite] Add backtracking test for `Load`.Gravatar Emilio Jesus Gallego Arias2018-03-10
|/ | | | Closes #6793.
* Merge PR #6946: Fix expected number of arguments for cumulative constructors.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6949: Revert PR #873: New strategy based on open scopes for ↵Gravatar Maxime Dénès2018-03-09
|\ \ | | | | | | | | | deciding…
| | * Fix expected number of arguments for cumulative constructors.Gravatar Gaëtan Gilbert2018-03-09
| |/ |/| | | | | | | | | | | We expected `nparams + nrealargs + consnrealargs` but the `nrealargs` should not be there. This breaks cumulativity of constructors for any inductive with indices (so records still work, explaining why the test case in #6747 works).
* | Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 23:02:01 +0000