aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* 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.
* 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
|\ \
* | | 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.
* | | 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
| | |/
* | / 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
| |/ |/|
* | Merge PR #6945: Fix error with univ binders on monomorphic records.Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6155: Get rid of ' notation for Zpos in QArithGravatar Maxime Dénès2018-03-09
|\ \ \
* \ \ \ Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\ \ \ \
* \ \ \ \ Merge PR #6328: Fix #6313: lost goals in nested ltac in refineGravatar Maxime Dénès2018-03-09
|\ \ \ \ \
* \ \ \ \ \ Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \
| | * | | | | More examples about shelve/given_up in tactic-in-terms.Gravatar Hugo Herbelin2018-03-08
| | | | | | |
| | * | | | | Proof engine: support for nesting tactic-in-term within other tactics.Gravatar Hugo Herbelin2018-03-08
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Tactic-in-term can be called from within a tactic itself. We have to preserve the preexisting future_goals (if called from pretyping) and we have to inform of the existence of pending goals, using future_goals which is the only way to tell it in the absence of being part of an encapsulating proofview. This fixes #6313. Conversely, future goals, created by pretyping, can call ltac:(giveup) or ltac:(shelve), and this has to be remembered. So, we do it.
* | | | | | Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | wish #4129)
| | | | | | | | * [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895.
| | | | | | | * Fix error with univ binders on monomorphic records.Gravatar Gaëtan Gilbert2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were declared twice for all records. Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an observable error for monomorphic records.
| | | | * | | | Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work
| | | | | * | | Add test-suite file for cumulative constructorsGravatar Matthieu Sozeau2018-03-08
| | | | | | |/ | | | | | |/|
* | | | | | | Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | |
* | | | | | | Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6903: [compat] Remove "Shrink Abstract"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
| | | | | * | | | | | | | [compat] Remove "Shrink Abstract"Gravatar Emilio Jesus Gallego Arias2018-03-06
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we the option "Shrink Abstract".
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-31 07:18:28 +0000