| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
And also clean INSTALL file of useless reminder of the procedure to
install using a package manager.
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
- fix the printers themselves after discharge was moved to the kernel
- change the test to make it more robust
In addition to checking that there is no "Error|Unbound" in the
output, ensure that the "go" function at the end of base_include
is defined. If there are any errors in base_include it won't be defined.
This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:
- change automatically included paths in Coqinit.init_ocaml_path to be
based on coqlib instead of coqroot. This way top_printers.ml and
base_include can find the compiled ml objects.
- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
add dependencies to test-suite/dune.
The dependencies should be calculated automatically once Dune has
better support for debug, or we implement proper support for test
printers.
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
|
|
|
|
obligation ones.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Remove other types of lines before copyright headers.
|
|
|
|
|
|
|
|
ml-style headers.
|
|
|
|
works on MacOS X
Reviewed-by: SkySkimmer
|
|
Works fine here, cc: #9975
|
|
|
|
Unfortunately, "+" regular expressions are not supported by default
with MacOS X's sed.
It is told that it would work with option -E though, but the syntax
seems then different.
|
|
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: vbgl
|
|
Reviewed-by: SkySkimmer
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
|
|
|
|
- Switch gtksourceview to 3.24.11
- Add appropriate set of icons and some other files GTK3 requires
- Add fix for ocamldebug so that this can be debugged
|
|
|
|
The stm.ml changes show that for the other classifications either the
vernac_when was ignored, or there was an assert on it forcing it to be
Now or Later depending on the vernac_type.
One may also note that the classification used in top_printers
`VtQuery,VtNow` would have failed those asserts...
|
|
|
|
Closes #10353
May be blocked on #10352
|
|
|
|
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.
|
|
Reviewed-by: aspiwack
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
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.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
|
|
|
|
I updated the readme example using the most recent overlay with only 1
touched development.
|
|
Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
|
|
|
