| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Redefine classical real numbers as a quotient of those constructive real numbers.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
|
|
|
|
Reviewed-by: Zimmi48
|
|
repository
Reviewed-by: SkySkimmer
Ack-by: ejgallego
|
|
This improves reproducibility of the CI environment.
The chosen commit has GTK+3 at 2.24.9.
|
|
Reviewed-by: SkySkimmer
|
|
This removes spurious Ack-by lines
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
The current code does some "opacification" for `Let`s, however that's
pretty fragile in general and not all codepaths do respect it.
We need to decide what to do.
|
|
Reviewed-by: SkySkimmer
|
|
creation.
Reviewed-by: herbelin
|
|
|
|
|
|
We can statically enforce that opaque definitions are always impure by
means of typing, leading to quite a few simplifications.
|
|
This is the last call to the kernel that makes a difference between opaque
definitions depending on their polymorphic status.
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
module.
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
command line (part 1)
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
|
|
Incidentally fix some missing newline in coqc help, and give proper
help for coqidetop and the "coq*worker"s.
|
|
This is now the "coqidetop" binary which specifically know how to
collect extra arguments.
|
|
- Binding coqc execution to the generic support for Coq binaries
(i.e. to start_coq).
- Moving init_toploop to the init part of coq executables so that coqc
can avoid to call it. By the way, it is unclear what workerloop
should do with it. Also, it is unclear how much the -l option should
be considered an coqidetop or coq*worker option. In any case, it
should be disallowed in coqc, I guess?
- Moving the custom init part at the end of the initialization
phase. Seems ok, despites the few involved side effects.
|
|
We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".
|
|
|
|
Incidentally moving parsing of "-batch" to the coqtop binary.
|
|
In particular, method init does not do parsing any more.
This allows for instance to let coqidetop treats itself the
"-filteropts" option.
|
|
|
|
A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
another query (this allows to get rid of the "exitcode" hack)
|
|
|
|
|
|
IMHO this functionality doesn't belong in the main code flow of
`Lemmas`, so for now we move it out to its own module, as a principle
to hopefully refactor it more.
We also do some very minor refactoring in `Lemmas`.
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
|
|
|
Fixes #10465
Following discussion we don't allow a generic `/usr/bin/python`
shebang anymore. We thus move all the scripts [but one] to python3,
and add python3 to the Azure base environment.
Unfortunately we still depend on python2 for the update-compat.py
script, see #10491
We thus have to complement #10467 adding python2 back to Nix,
until #10491 is fixed.
|
|
for list prints in gramlib
Reviewed-by: ejgallego
|
|
Compcert needs a new menhir.
|
|
Order
Reviewed-by: Zimmi48
|
|
gramlib
This means we don't need to ignore the result of the fold. cf #10471
Using Format.pp_print_list instead of a custom iteri was suggested by
Jean-Christophe Léchenet (eponier)
|
