| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
Reviewed-by: gares
|
|
|
|
|
|
|
|
We move the role data into the evarmap instead.
|
|
Reviewed-by: ejgallego
|
|
|
|
Closes #10353
May be blocked on #10352
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
We rename modify to map [more in line with the rest of the system] and
make the endline function specific, as it is only used in one case.
|
|
We refactor the terminator API to make it more internal. Indeed we
remove `set_terminator` and `get_terminator` is only there due to
access to internals in the STM `save_proof` path by the infamous
`?proof` parameter.
After this only 2 non-standard terminators remain: obligations and
derive. We will refactor those in next PRs.
|
|
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
|
|
vernac syntax
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: herbelin
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
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.
|
|
This is to avoid depending on the combination "Discharge" + no opened
section to trigger an automatic declaration of instance.
|
|
I don't know what goal_selector.v was supposed to test but CI says
nobody relied on it.
|
|
interpretation scopes
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
|
|
|
|
Slight improving of style in passing.
|
|
We deprecate -require (= Require Import) to avoid the confusion with Require.
We propose a regular equivalent to all vernac variants in expanded and
short version:
-require-import, -require-export
-require-import-from, -require-export-from
-ri, -re
-rifrom, -refrom
We also add -rfrom, but wait for the end of deprecation of -require to
replace -load-vernac-object by -require and to introduce a shorthand
-r for the new -require.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: maximedenes
|
|
|
|
side-effects
Reviewed-by: SkySkimmer
|
|
|
|
This matches the makefile build with -warn-error.
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
explain more
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
Ack-by: tlringer
|
|
Reviewed-by: ejgallego
Ack-by: gares
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
Reviewed-by: vbgl
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
Instead of having the monormorphic universes from the immediate
data separated from the ones from the body, we only rely on the
former. There is no reason to delay given that the body is always
force upfront.
|
