| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
+ hide interp_functional_vernac in vernacentries
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
vernac
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
- 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 ;_;
|
|
generalization + cleanups
Reviewed-by: herbelin
|
|
|
|
|
|
We cleanup a bit the implementation of LoadPath which is not possible
as now all the loadpath logic is in the same place.
In particular, we remove exceptions in favor a `locate_result` monad.
More cleanup should still be possible, in particular
`locate_absolute_library` and `locate_qualified_library` should be
merged.
|
|
|
|
|
|
|
|
|
|
|
