| Age | Commit message (Collapse) | Author |
|---|
|
- Add an instance to ZifyInst to instruct zify that
0 < x -> 0 < y -> 0 < Z.pow x y
- More aggressive interval analysis to bound non-linear monomials.
|
|
|
|
|
|
It seems broken according to unicoq experiences https://gitter.im/coq/coq?at=5e0e3e0005298604982ac3f7
Building cmxa of mlpack is already this way.
|
|
Closes #10491
We re-add the header in doc/tools/coqrst/notations/fontsupport.py
which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6
The fontsupport script itself has been kept for reference, however it
is not involved by any build target as of today.
|
|
clauses in pattern matching decompilation algorithm
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.
|
|
This way when users `Import EqNotations`, we get pretty-printing for
equality `match` statements too.
|
|
This form is only used in coq-bignums and not documented. I think
removal is the best choice, specially as `zify` is not part of the
omega plugin anymore.
|
|
Changes to the test-suite were backported from PR #11288.
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
|
|
Fixes #9532
Fixes #9490
|
|
This change improves the relaxed ambiguous path condition of coercions (#9743)
to check that any circular inheritance path of `C >-> C` is definitionally equal
to the identity function of the class `C`. Moreover, for a new inheritance path
`p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not
report the ambiguity of `p` and `q` if they have a common element, that is to
say:
`p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2`
for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`.
In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be
checked; thus, checking the ambiguity of `p` and `q` is redundant with them.
If the new mechanism does not report any ambiguous path, the inheritance graph
must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]:
1. for any circular path `p : C >-> C`, `p` is definitionally equal to the
identity function, and
2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible.
[Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95,
LNCS, vol 1158, Springer, 1996, pp 1-15.
[Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance,
In: POPL '97, ACM, 1997, pp 292-301.
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
|
|
non-resolvable, always
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.
Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.
Fixes #11063 and fixes #11242 and fixes #11270
|
|
Check that we don't regress on PR #10762 example
Fix regression discovered by Arthur in PR #10762
Fix script of #10298 which was relying on breaking semantics for `eapply`
Add doc
Add comment in clenvtac
Actually, always mark shelved goals as unresolvable
Update doc to reflect semantics w.r.t. shelved subgoals
|
|
Split from #10331
Fix part of #8196
Replaces #9343
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
|
|
|
|
Fixes #10971
|
|
Ack-by: Zimmi48
Ack-by: herbelin
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Failing on CProdN([],...) was maybe a bit too radical.
|
|
|
|
doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst
OK, thanks.
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.
Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.
Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.
|
|
Reviewed-by: JasonGross
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
The missing dependency impacted the algorithm for detecting default
clauses.
|
|
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
in order to make builds reproducible.
See https://reproducible-builds.org/ for why this is good
and https://reproducible-builds.org/specs/source-date-epoch/
for the definition of this variable.
Fixes #11037
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
|
|
Types of changes are defined in the list defined by Keep a Changelog
1.0.0 (https://keepachangelog.com/en/1.0.0/):
- Added
- Changed
- Deprecated
- Fixed
- Removed
We exclude the type Security for now, even for soundness fixes,
because the process of handling security vulnerabilities is different
from anything we follow right now.
|
|
|
|
`DelPath`
Reviewed-by: ejgallego
|
|
|
|
regression).
|
|
This increases backwards compatibility. If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.
|
