| Age | Commit message (Collapse) | Author |
|---|
|
proof data on top of declare.
Reviewed-by: ppedrot
|
|
exception names
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
flags.
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
makefile fixes
Reviewed-by: ejgallego
Reviewed-by: vbgl
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Non-delayed entries can be done with the current constructor, delayed
ones will require more work.
|
|
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: ppedrot
|
|
And add links to UI in the browser.
|
|
|
|
check_constant_declaration
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Fixes #10640
We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.
No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.
Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.
|
|
|
|
|
|
|
|
sig_not_dec
Reviewed-by: herbelin
|
|
|
|
- remove the architecture component (we don't do anything
arch-specific so it was just a rewording of int_size)
- have configure tell the make build system about int_size instead of
reimplementing cp
As a bonus, add the copyright header to uint63.mli.
|
|
Reviewed-by: Zimmi48
|
|
This improves error reporting. Addendum to #10515
|
|
Instead of doing (simplified code)
~~~ocaml
let check env kn cb =
let flags = env.flags in
let env' = set_flags env cb.flags in
...
let env = add_constant cb kn (if poly then env else env') in
set_flags env flags
~~~
(NB: when not poly env' has only the typing flags different from env)
we do
~~~ocaml
let check env kn cb =
let env = set_flags env cb.flags in
...
()
let check env kn cb =
let () = check env kn cb in
add_constant cb kn env
~~~
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Now everything that does not have any dependencies goes to the first stage.
The rest goes to the first stage following all its dependencies.
All jobs specifying a dependencies keyword also specify a needs keyword.
|
|
Reviewed-by: Zimmi48
|
|
Master version of the fix for #10679
|
|
|
|
We go back to the kind of workflow we had in CircleCI thanks to GitLab
12.2 new needs keyword.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
Reviewed-by: mattam82
|
|
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.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
TLC and CPDT are not actually tested. No point in keeping them as if they were.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: ejgallego
|
|
deployed versions.
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.
|
|
|
|
We update the URLs to the new ones, even if the previous continue to work.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
