| Age | Commit message (Collapse) | Author |
|---|
|
This allows to refer to them from other part of the manual without any ambiguity.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: cpitclaudel
|
|
From the CHANGES file in branch v8.9.
|
|
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: vbgl
|
|
CoqIDE.
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
|
|
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
|
|
- 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
|
|
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
|
