| Age | Commit message (Collapse) | Author |
|---|
|
I'd say this is more of a temporary measure than a long-term plan; IMO
we should make the interfaces safe so `Gramlib.Grammar` does provide
only one signature.
|
|
|
|
This makes sense as a step towards a more functional handling of the
state.
|
|
If we need more fine-tuning we should manage the warnings with the
standard Coq mechanism.
|
|
Latest refactorings allow us to make the signature Coq parser a
standard `Grammar.S` one; the only bit needed is to provide the extra
capabilities to the `Lexer` signature w.r.t. to comments state.
The handling of Lexer state is still a bit ad-hoc, in particular it is
global whereas it should be fully attached to the parsable. This may
work ok in batch mode but the current behavior may be buggy in the
interactive context.
This PR doesn't solve that but it is a step towards a more functional
solution.
|
|
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
|
|
This is not needed anymore after the unification.
|
|
We remove Coq's wrapper over gramlib's grammar constructors.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
See https://github.com/ocaml/ocaml/issues/7842
|
|
Reviewed-by: ejgallego
|
|
IMHO it is a bit more logical, WDYT?
|
|
Remove unneeded source and output files
Move all commands under command NT
Add a lot of edits for commands and tactics
|
|
Ack-by: Zimmi48
|
|
|
|
Fixes #11905
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
|
|
|
|
Print 1.5 as 1.5 and not 15e-1.
We choose the shortest representation
with tie break to the dot notation (0.01 rather than 1e-3).
The printing remains injective, i.e. 12/10 is not mixed with 120/100,
the first being printed as 1.2 and the last as 1.20.
|
|
Print 1.5 as 1.5 and not 15e-1.
We choose the shortest representation
with tie break to the dot notation (0.01 rather than 1e-3).
The printing remains injective, i.e. 12*10^2 is printed 12e2 in order
not to mix it with 1200 and 12/10^1 is not mixed with 120/10^2, the
first being printed as 1.2 and the last as 1.20.
|
|
The Docker image coqorg/coq:dev is currently built using the OPAM file
coq.opam. Since this file is used for develoment purpose, it would be
better to use a more stable one for building the docker images. The
OPAM option "--locked=docker" will then be used in the opam pin
command when building the docker image to use the new coq.opam.docker
file.
The new file builds Coq using make, this is temporary and could be
reverted to dune once it supports "-native-compiler yes".
|
|
The current API does just exist as a workaround for a bug.
|
|
Steps towards unification with `DeclareDef` API.
|
|
Steps towards unification with `DeclareDef` API.
|
|
We move `Recthm` to `DeclareDef` so it is shared by interactive and
direct fixpoint declaration.
This is the last step before unifying both paths.
|
|
Note that we had to introduce a `restrict_ucontext` parameter to be
faithful to the implementation in obligations, however this looks like
a bug.
|
|
|
|
|
|
|
|
First commit of a series that will unify (and enforce) the handling of
mutual constants. We will split this in several commits as to easy
debugging / bisect in case of problems.
In this first commit, we move the actual declare logic to a common
place.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Thanks to `.ocamlformat-ignore`, we can call ocamlformat blindly but
only the non-ignored files will be affected.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
coq_config
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
|
|
|
|
They were defined at level 70, no associativity in all but three places,
where they were instead declared at level 35.
Fixes #11890
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: gares
|
