| Age | Commit message (Collapse) | Author |
|---|
|
obligation ones.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.
|
|
|
|
We move the role data into the evarmap instead.
|
|
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: 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.
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
We remove unused parts of the API, almost all of them belonging to the
legacy engine. This was detected using coverage testing.
The list is provisional and should be subject to change, let's see
what CI says.
|
|
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Using pstate makes no sense for printing global stuff
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
This was dead code.
|
|
This is actually dead code, we never observe it.
|
|
This is just moving code around, so it should not change the semantics.
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Fixes #9919.
|
|
If the reduction function is known not to depend on the named context,
then we can perform it in parallel on the various variables.
|
|
|
|
|
|
|
|
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
|
|
This prevents having to call global functions, for no good reason.
We also seize the opportunity to name the check argument.
|
|
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.
|
|
Reviewed-by: ppedrot
|
|
as assumptions
Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers
|
|
(Merge of the initial version with #9983 was broken)
|
|
We add a fast path when generalizing over variables.
|
|
|
|
The creation of the local hint db now inherits the union of the modes
from the dbs passed to `typeclasses eauto`.
We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned-up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
already there.
Reviewed-by: gares
|
|
|
