| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Reviewed-by: jfehrle
|
|
clauses in pattern matching decompilation algorithm
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
Vernacular section to prodns
Reviewed-by: Zimmi48
|
|
productions in a prodn
Ack-by: Zimmi48
Ack-by: cpitclaudel
|
|
unification error message
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
|
|
|
|
|
|
Reviewed-by: MSoegtropIMC
|
|
functionality
Reviewed-by: CohenCyril
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Co-Authored-By: Cyril Cohen <CohenCyril@users.noreply.github.com>
|
|
The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
Ack-by: maximedenes
|
|
Reviewed-by: Zimmi48
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
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
|
|
Closes #11225 , we use a bit of a hack due to the way the Makefile
installs this plugin.
|
|
Most workers these days have 1 core, and building bedrock with 2 cores
in that setup seems to be too memory stressful.
|
|
Reviewed-by: ejgallego
|
|
clearer.
|
|
Might be improvable further. In the first example, we have two
environments involved and one is implicit. It does not seem excluded
that a variable name of the second environment shows up which is not
listed in the first environment.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
- remove manual flexlink circular dependency handling
- use standard configure process instead of hand made windows make files
- enable parallel build
- remove bootstrapping step (maybe should be there for release builds)
|
|
Reviewed-by: jfehrle
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
We restrict to those that are actually related to typeclasses, and
perform the following renamings:
Classops --> Coercionops
Class --> ComCoercion
|
|
|
|
This highlights the fact that diamond inheritance of a custom entry
is a tricky problem, as well as merely importing two custom entries with
the same name from two different modules. The only sane way to give a
semantics to that is to stick to module-scoped objects, i.e. give those
entries a kernel name. In the meantime, I went for a warning when
overriding entries.
|
|
|
|
(Fixes #11321)
It has the added advantage of performing 6 less 64-bit operations per
long multiplication.
|
|
The sign bit is supposed to be zero, so no need to mask it out. If it was
not zero, most of the algorithms in this file would fail horribly.
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: gares
|
|
|
|
Fixes #9532
Fixes #9490
|
|
Reviewed-by: gares
|
|
|
|
representation.
Reviewed-by: maximedenes
|
|
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.
|
|
|
