| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
happened at initialization time
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
NB: I made .aux be cleaned only with distclean imitating the main Makefile.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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)
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|/
|
|
|
| |
We take into account all future ipats, not just the ones in
the current branch
|
|\
| |
| |
| | |
removing the test.
|
|\ \ |
|
|\ \ \ |
|
| |/ /
|/| | |
|
|\ \ \
| | | |
| | | |
| | | | |
looking for a notation for a nested pattern
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We also make the code of [compact] in kernel/univ.ml a bit clearer.
|
| | | | | | |
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | | |
Since this is an open bug, it is of lesser importance but
non-deterministic tests are a real problem OTOH.
|
|\ \ \ \ \
| |_|/ / /
|/| | | | |
|
|\ \ \ \ \ |
|
| |_|/ / /
|/| | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
|/ / / / |
|
|\ \ \ \ |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |
|
| |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |/ /
| | |
| | |
| | |
| | | |
This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.
|
|\ \ \ |
|
|\ \ \ \ |
|
| | |/ / |
|
| | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/
|/|
| |
| | |
For instance, error in "Goal forall a f, f a = 0" is now located.
|
|/
|
|
| |
Closes #6793.
|
|\ |
|
|\ \
| | |
| | |
| | | |
deciding…
|
| |/
|/|
| |
| |
| |
| |
| | |
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).
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| | |
notation to use among several of them"
This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing
changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
|
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|\ \
| |/
|/| |
|
|\ \ |
|
| | | |
|
| |/
|/| |
|