| Age | Commit message (Collapse) | Author |
|---|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
|
|
Closes #13794
|
|
Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
|
|
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
section/module closing time
Reviewed-by: SkySkimmer
|
|
|
|
Fixes #13755 .
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
The goal is to eventually only use the Simplex solver and
remove all the code needed for fourier elimination.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: ppedrot
|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
|
|
at ..." instead)
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
(use "with ... at ..." instead)
|
|
Reviewed-by: herbelin
Ack-by: ejgallego
|
|
Reviewed-by: gares
|
|
|
|
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
Reviewed-by: herbelin
|
|
|
|
We additionally check that occurrence 0 is invalid in simpl at,
unfold at, etc.
|
|
|
|
Otherwise we pay a high cost for printing that might never make it to
the user.
|
|
Fix #13595
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
Following a request from Pierre-Marie Pédrot in #13258
|
|
It was generating a completely nonsense case branch, but for some reason
the proof still went trough.
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
|
|
Reviewed-by: mattam82
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
Reviewed-by: vbgl
|
