| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: herbelin
|
|
|
|
There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v
* comment the implementations with loop invariants to enable an easy
pen&paper proof of correctness (note to reviewers: the one in
uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
(only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
(cmp is computed at the end of the first loop rather than at the beginning,
potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
new specifiation of div21
* add a test
|
|
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
We add a fast path when generalizing over variables.
|
|
It was fairly easy, the plugin defined an argument that was only used in
a vernacular extension. Thus marking it as VERNAC was enough not to link
to Ltac.
|
|
Co-Authored-By: Blaisorblade <p.giarrusso@gmail.com>
|
|
Copy change's variants in change_no_check, since supposedly they should all be
supported. But they haven't been tested, and my example fails.
|
|
Triggered by trying to understand https://gitlab.mpi-sws.org/iris/iris/merge_requests/235.
- Add a new section at the end
- Document change_no_check, and convert_concl_no_check, address review comments
|
|
Ack-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
The creation of the local hint db now inherits the union of the modes
from the dbs passed to `typeclasses eauto`.
We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned-up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
The OPAM build has been broken it seems since almost the beginning as
OPAM doesn't substitute variables in the almost undocumented
`build-env` form.
Packages built this way worked as Coq used a different method to
locate `coqlib`, however the value for `coqlib` was incorrect.
We set instead the right prefix using an explicit configure call.
|
|
A module allowing the user to build a UsualDecidableTypeFull from a pair
of such, exactly analogous to the extant PairDecidableType and
PairUsualDecidableType modules.
Co-authored-by: Jean-Christophe Léchenet <eponier@via.ecp.fr>
|
|
We also update the plugin tutorial.
This was already tried [in the same exact way] in #8811, however the
bench time was not convincing then, but now things seem a bit better,
likely due to the removal of some extra normalization somewhere.
Some more changes from #8811 are still pending.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Currently this env is only used to error for Printing If/Let on
non-2-constructor/non-1-constructor types so we could alternatively
remove it and not error / error later when trying to print.
Keeping the env and the error as-is should be fine though.
|
|
This was introduced by @herbelin in
817308ab59daa40bef09838cfc3d810863de0e46, appears to have been
made unnecessary again by herbelin in
4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6.
At this point it appears to be completely unused.
|
|
|
|
This is to be consistent with what the preference panel displays (namely μpG).
We keep the nanoPG name in the preference file by compatibility.
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
|
|
|
|
|
|
PR #8187 misplaced its CHANGES entry. We remove it in this commit instead
of moving it to the right place because it is reverted in #9987.
|
|
|
|
|
|
Add more links to PRs and credits of authors.
|
|
|
|
|
|
Mainly markup fixes by Theo
Co-Authored-By: mattam82 <matthieu.sozeau@inria.fr>
|
|
|
|
ProofGeneral (master branch)
Reviewed-by: ejgallego
|
|
`nonPropType` interface
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ggonthier
|
|
In particular, we explicitly mention the existence of an Emacs mode.
|
|
On MacOS X: Ctrl-Cmd-Left and Ctrl-Cmd-Right
Elsewhere: Meta-Left and Meta-Right
See issue #9899 (moving cursor to beginning and end of file).
|
