| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
| |
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | | |
This is useful as it allows to reflect program_mode behavior as an attribute.
|
| |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | |/ |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Thanks to @SkySkimmer for lots of comments and bug-finding.
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | | |
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
|
|\ \ \ \ |
|
| |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | | |
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In the transition towards a less global state handling we have the
necessity of mix imperative setting [notably for the modules/section
code] and functional handling of state [notably in the STM].
In that scenario, it is very convenient to have typed access to the
Coq's `summary`. Thus, I reify the API to support typed access to the
`summary`, and implement such access in a couple of convenient places.
We also update some internal datatypes to simplify the `frozen` data
type. We also remove the use of hashes as it doesn't really make
things faster, and most operations are now over `Maps` anyways.
I believe this goes in line with recent work by @ppedrot.
We also deprecate the non-typed accessors, which were only supposed to
be used in the STM, which is now ported to the finer primitives.
|
|/ /
| |
| |
| |
| |
| |
| |
| | |
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
In particular we must invalidate the state cache in the case of an
exception.
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.
E.g mono@{i} := Type@{i} is printed as
mono@{mono.i} := Type@{mono.i}.
There can be a name clash if there's a module and a constant of the
same name. It is detected and is an error if the constant is first
but is not detected and the name for the constant not
registered (??) if the constant comes second.
Accept VarRef when registering universe binders
Fix two problems found by Gaëtan where binders were not registered properly
Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs
Fix an issue of the stronger restrict universe context + no evd leak
This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
|
|\ \
| | |
| | |
| | | |
functionalization.
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
instance.
|
| |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.
We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.
This is a preliminary step for the work on attributes.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | | |
In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.
|
|\ \ \ \ |
|
| |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Fixes #6130, it was a silly omission from a previous output
refactoring.
We redirect all channels as this was the implied semantics of the old
command.
|
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \
| |_|_|/
|/| | | |
|
| | | | |
|
| | | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
In particular, we put all the context in the atts structure, and
generalize the type of the parameters of a vernac.
I hope this helps people working on "attributes", my motivation is
indeed having a more robust interpretation.
|
|\ \ \ |
|
|\ \ \ \ |
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Note that this makes the following syntax valid:
Axiom foo@{i} bar : Type@{i}.
(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
|
| | | | |
|
| | | | |
|
| | | | |
|
| |/ /
|/| |
| | |
| | |
| | | |
We also remove some internal implementation details from the mli file,
there due historical reasons.
|
| | |
| | |
| | |
| | |
| | |
| | | |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
| | |
| | |
| | |
| | |
| | | |
I think this only affects printing (in the new test you would get
[Var (0)] when printing runwrap) but is still ugly.
|