| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: JasonGross
|
|
Reviewed-by: gares
Ack-by: ppedrot
Ack-by: ejgallego
|
|
Close #14074
|
|
|
|
This removes the need for the remote counter.
|
|
The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints. The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.
Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once
Co-authored-by: Andrej Dudenhefner <mrhaandi>
Closes #12184, #11656
|
|
Reviewed-by: vbgl
|
|
The vernacular command takes a reference instead of a constr.
Moreover, the head symbol is checked i.e
Add Zify InjTyp ref checks that the referenced term has type
Intyp X1 ... Xn
Closes #14054, #13242
Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
|
|
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.
|
|
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
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.
|
|
Reviewed-by: gares
|
|
to check for conversion
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Fixes #14003: Ltac2 redefinition check is broken.
|
|
Reviewed-by: ppedrot
|
|
notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
Fixes #13963
|
|
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.
|
|
The table of coercion classes (`class_tab`) has been extended with information
about reachability. The conversion checking of a pair of multiple inheritance
paths (of coercions) will be skipped if these paths can be reduced to smaller
adjoining pairs of multiple inheritance paths, and this reduction will be
determined based on that reachability information.
|
|
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: SkySkimmer
Ack-by: jfehrle
|
|
|
|
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC
|
|
|
|
|
|
|
|
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.
|
