| Age | Commit message (Collapse) | Author |
|---|
|
* This commit add float instructions to the VM, their encoding in bytecode
and the interpretation of primitive float values after the reduction.
* The flag '-std=c99' could be added to the C compiler flags to ensure
that float computation strictly follows the norm (ie. i387 80-bits
format is not used as an optimization).
Actually, we use '-fexcess-precision=standard' instead of '-std=c99'
because the latter would disable GNU asm used in the VM.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
AFAICT the reasoning for introducing this function doesn't hold
anymore. This is needed for future refactorings that should make some
types private.
|
|
|
|
the kernel.
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
|
|
|
|
|
|
Opening up a lambda should always lift the substitution attached to it.
|
|
Reviewed-by: JasonGross
Reviewed-by: gares
Ack-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
They probably don't need to be executable
|
|
Explain into the release process how to prepare the release notes.
|
|
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: vbgl
Reviewed-by: SkySkimmer
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
proof data on top of declare.
Reviewed-by: ppedrot
|
|
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.
We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.
cc: #7560
|
|
Reviewed-by: SkySkimmer
|
|
We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.
Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.
Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.
I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.
|
|
TLC and CPDT are not actually tested. No point in keeping them as if they were.
|
|
Reviewed-by: ejgallego
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
|
