| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Ack-by: jfehrle
|
|
instead of catching `Not_found`
Reviewed-by: ppedrot
|
|
catching `Not_found`
`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.
|
|
For some reason I was confusing the position and the level in the previous
version of the code.
Fixes #11866: Ltac2 Notations do not respect precedence.
|
|
Reviewed-by: JasonGross
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Ack-by: SkySkimmer
Ack-by: olaure01
|
|
|
|
At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.
|
|
|
|
The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.
We fix this by adding dummy parameter arguments on sight.
Fixes #14009: TC search failure with primitive projections.
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`. Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.
Fixes #14011
|
|
Bytecode execution of persistent arrays can modify structured values meant
to be marshalled in vo files. Some VM values are not marshallable, leading
to this anomaly.
There are further issues with the use of a hash table to store structured
values, since they rely on structural equality and hashing functions.
Persistent arrays are not safe in this context.
Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
|
|
Fixes #14003: Ltac2 redefinition check is broken.
|
|
Reviewed-by: SkySkimmer
|
|
transitively closed
Reviewed-by: ppedrot
|
|
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
|
|
Fixes #12806: Ltac2 Notation's open_constr should accept scope stacks.
|
|
Instead of recomputing the n-th lifts of terms for every subterm under a context,
we introduce a table storing the value of this lift across contexts. While not
the most efficient algorithmically, it is still much more efficient in practice and
does not exhibit the exponential behaviour of replacing under different subcontexts.
In an ideal world we would have an equality function on terms that allows to compute
equality up to lifts, which would prevent having to even compute the lift at all, but
the current fix has the advantage to be self-contained and not require dangerous
tweaking of an equality function which is already complex enough as it is.
Fixes #13896: cbn very slow.
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
|
|
Fix #13903
|
|
Reviewed-by: ppedrot
|
|
|
|
ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"
Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.
|
|
This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.
Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.
(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
|
|
|
|
Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.
This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.
|
|
Reviewed-by: ppedrot
|
|
Fixes #13755 .
|
|
We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.
|
|
This returns to the previous behaviour of Implicit Type forgetting
universes.
`Implicit Type T : Type@{u}.` may be confusing as it is equivalent to
`: Type`, but until we have a better idea of what to do with anonymous
types I see no other solution, especially in the short term to fix the
bug.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
|
|
Fixes #3166.
|
|
|
|
cumulative inductive types
Reviewed-by: SkySkimmer
|
|
Reviewed-by: herbelin
|
|
types
|
|
|
|
check resolution of evars more incrementally
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ppedrot
|
|
incrementally.
The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.
|
|
|
|
Reviewed-by: ejgallego
|
|
of universes in "Context"
Reviewed-by: SkySkimmer
|
|
Fixes #13453 which was a loop in
~~~ocaml
let normalize a =
let o = optims () in
let rec norm a =
let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
if eq_ml_ast a a' then a else norm a'
in norm a
~~~
the `eq_ml_ast` was always returning `false`.
|
|
|
|
|
