| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
|
|
Apparently `expr 1 \+ 1` is fine on Linux but not cygwin/Windows, where
it fails with "syntax error". Similarly for `-` and `/`.
|
|
This reverts commit ec505a2fa67b0776b624be54417e06c6512f1734.
A better fix is coming
|
|
Apparently the bogomips produced by cygwin are extra-bogo.
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
|
|
Ack-by: ejgallego
|
|
Reviewed-by: maximedenes
|
|
|
|
|
|
For now, the API is unchanged and this commit only splits pretyping code for
each glob_constr constructor into a record field.
|
|
|
|
|
|
Issue #10603
|
|
Reviewed-by: ejgallego
|
|
|
|
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
|
|
Reviewed-by: maximedenes
|
|
Fix #11266
|
|
avoid possible "breach of privacy"
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
take only the template_check flag instead of the whole env
|
|
We do [solve_remaining_evars all_and_fail_flags] immediately before
calling [interp_mutual_inductive_constr] so these checks are extra.
|
|
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
