| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
| | | | |
|
| | |/
|/|
| |
| | |
Before sometimes there were lists and strings.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
The primary concern is for clarity of reading.
May it affects tools which would parse the output of "Print LoadPath"?
Presumably, these tools would not support file names with spaces
already, so this may have no impact.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a continuation on #6183 and another step towards a more
functional interpretation of commands.
In particular, this should allow us to remove the locality hack.
|
Maxime Dénès
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Matthieu Sozeau
Matthieu Sozeau
Hugo Herbelin