| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
|
|
* This patch is a quick fix that removes part of the features of coq/coq#10022,
namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
relation R. This just means we'll need to do an extra step [rewrite UnderE.]
which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23
|
|
Reviewed-by: Zimmi48
Ack-by: maximedenes
|
|
This should have been running already, but it was forgotten in #9872
|
|
This way when users `Import EqNotations`, we get pretty-printing for
equality `match` statements too.
|
|
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.
|
|
|
|
Integrate merging doc in the main contributing document.
|
|
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
|
|
It was decided during the Coq WG that code owner teams are more
convenient, in particular because they allow adding and removing team
members without going through a pull request. For each team, we
should aim to have at least three code owners, even if in some cases
we are going to start with less.
We also stop triggering review requests for changelog entries as was
also decided during the WG.
|
|
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
|
|
|
|
We cannot use caml_alloc_small because the macros Setup_for_gc and
Restore_after_gc are still relevant (and critical). This means defining
the CAML_INTERNALS macro, but it is a legit use and actually documented
in the OCaml manual.
This will help with forward compatibility with OCaml compilers, e.g.,
issue #10603. Unfortunately, it also means that we can no longer use #9914
to prevent memory corruption.
The old macro is still used for OCaml versions prior to 4.10, as the
upstream macro might process Ctrl+C when it is called.
|
|
Instead of relying on the Coq_config immutable flag, we introduce an
initialization-only flag to govern the use of the native compiler. This
allows to make coqc passed with "-native-compiler no" behave as if it had
been configured without native compilation.
|
|
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.
|
|
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
|
|
|
|
|
|
(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.
|
|
|
