| Age | Commit message (Collapse) | Author |
|---|
|
Apart from being an ugly hack in the kernel, the universe-adding function
is already robust to redundant universes anyways.
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
Instead of various termops and globnames aliases.
|
|
The previous system was from before globref was in the kernel.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
This was the only part in the kernel that really relied on the contents
of the Monomorphic node.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
extraction.
Reviewed-by: maximedenes
|
|
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
|
|
|
|
Performance bug of PrimFLoat.compare with native_compute
When adapting Coq.Interval with @erikmd and @silene, we noticed that
PrimFLoat.compare is taking a lot of time with native_compute (much
more than with vm_compute).
This comes from the implementation using the OCaml polymorphic
comparison instead of the float comparison.
|
|
Instead, we export in Safe_typing the current module declaration.
|
|
Not sure if it's possible to see it without a plugin.
|
|
- allow viewing the internal representation of uglobal and universe
(with universe, this replaces the "map" function. I kept exists and
for_all as they felt somewhat convenient)
- add universe set and map modules (currently unused but they're natural)
|
|
|
|
|
|
|
|
preparation for direct discharge
|
|
|
|
We make a temporary directory for these files and cleanup at process
exit. The temporary directory means we don't have to guess what
extensions ocaml will produce, we can just delete everything there.
We use Lazy to avoid spamming unused directories when ahead-of-time
compiling without actually using native casts / nativenorm (typically
stdlib files).
Sadly ocaml has "create temp file" but not "create temp dir", so we
have to copy the name generation code.
Fix #10495
|
|
This doesn't actually have anything to do with positivity AFAICT, we
just want the number of non-parameter arguments.
|
|
|
|
|
|
|
|
(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.
|
|
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Issue #10603
|
|
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
|
|
This is a follow up of #11010 ; I've realized that for example in #11123
a large part of the patch is detabification as indeed the files are
mixed in tabs/space style so developers are forced to do the cleanup
each time they work on them.
Command used:
```
for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
Checked empty diff with `git diff --ignore-all-space`
|
|
This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
|
and do not run template_candidate in the upper layers when the
template attribute is given.
This means we can use an over-approximation in the upper layer
implementation of template_candidate (returning false even in cases
which the kernel may accept) if we ever want to.
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
