| Age | Commit message (Collapse) | Author |
|---|
|
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
|
|
|
|
This datatype does belong to this layer.
|
|
We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:
- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
pushed upwards]
We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.
More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
|
|
in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
#10205.
Reviewed-by: cpitclaudel
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
These were found with the following command:
$ git grep "1999-" | grep -v "2019"
|
|
Remove other types of lines before copyright headers.
|
|
|
|
|
|
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: tlringer
|
|
|
|
This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual
After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.
Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
|
|
Reviewed-by: cpitclaudel
|
|
This allows to refer to them from other part of the manual without any ambiguity.
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: cpitclaudel
|
|
From the CHANGES file in branch v8.9.
|
|
|
|
|
|
CoqIDE.
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
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
|
|
vernac syntax
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: herbelin
|
|
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.
|
|
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.
|
|
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
