aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* 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.
* Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Gravatar Hugo Herbelin2018-04-26
|
* 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
|
* 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
|\ \ \ \ \
| | * | | | 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 #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.
* | / 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
|\ \
| | * Revert "Merge PR #873: New strategy based on open scopes for deciding which ↵Gravatar Maxime Dénès2018-03-09
| |/ |/| | | | | | | | | | | notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
| * Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified.
| * Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.
| * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
* | Merge PR #6480: Allow Prop as source for coercionsGravatar Maxime Dénès2018-03-09
|\ \ | |/ |/|
* | Merge PR #6895: [compat] Remove "Refolding Reduction" option.Gravatar Maxime Dénès2018-03-09
|\ \
| | * added test for coercion from typeGravatar charguer2018-03-09
| | |
| | * allow Prop as source for coercionsGravatar charguer2018-03-09
| |/ |/|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 00:01:10 +0000