| Age | Commit message (Collapse) | Author |
|---|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
|
(by the checker refactor AFAICT)
+ fix commit for the coqtop side fix (it got rebased at some point)
Close #10705
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Opening up a lambda should always lift the substitution attached to it.
|
|
|
|
Explain into the release process how to prepare the release notes.
|
|
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
|
|
|
|
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.
|
|
|
|
And also clean INSTALL file of useless reminder of the procedure to
install using a package manager.
|
|
|
|
The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.
This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.
Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.
As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.
We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
|
|
Formerly, knowing if a declaration was to be discharged, to be global
but invisible at import, or to be global but visible at import was
obtained by combining the parser-level information (i.e. use of
Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use
of Local vs Global) with the result of testing whether there were open
sections.
We change the meaning of the Discharge flag: it does not tell anymore
that it was syntactically a Variable/Hypothesis/Let, but tells the
expected semantics of the declaration (issuing a warning in the
parser-to-interpreter step if the semantics is not the one suggested
by the syntax). In particular, the interpretation/command engine
becomes independent of the parser.
The new "semantic" type is:
type import_status = ImportDefaultBehavior | ImportNeedQualified
type locality = Discharge | Global of import_status
In the process, we found a couple of inconsistencies in the treatment
of the locality status. See bug #8722 and test file LocalDefinition.v.
|
|
|
|
|
|
- use coqc instead of coqtop (since -compile doesn't work anymore this
is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users
The dune-dbg dependencies are still broken ;_;
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: vbgl
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
|
|
Move existing entries.
|
|
Reviewed-by: maximedenes
|
|
Ack-by: Zimmi48
Reviewed-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
|
|
|
|
The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.
As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.
We don't mark deprecation as fatal as to allow time for migration.
Fixes #6974
|
|
|
|
|
|
|
|
Since e1e7888, stuck projections were not computed correctly.
Fixes #9684
|
|
Reviewed-by: cpitclaudel
Reviewed-by: vbgl
|
|
|
|
|
|
- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v
- test-suite/failure/inductive4.v is now .../inductive.v
- repro for #4157 now added to the repo (it was in an unmerged commit
on @herbelin's repo)
- commit message of 244d7a9aa contains a repro for its bug (I didn't
bother adding to the test suite as a return of the bug could just as
well use different strings so the specific repro wouldn't test
anything useful)
|
|
|
|
to an archive subfolder.
Reviewed-by: ejgallego
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
subfolder.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
We add a shim for running the byte version of coqtop. This fixes the
Coq part of #9727 , the Dune part is still open at
https://github.com/ocaml/dune/issues/108 but this PR includes a
workaround.
Unfortunately we have to introduce a small inefficiency in the build
process as we build both byte and native versions of plugins for this
work reliable.
As this is a choice done during bootstrap it won't be easy to fix
until we have our own `dune coqtop` command and we can control the
rules depending on the final target.
This should affect the `check` target so still fast builds should be
possible, but if this is a problem we could add a `byteboot` target to
help.
|
