| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
Typeclasses.typeclass
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ \
| | | |
| | | |
| | | | |
same right-hand side.
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.
Adding options
Unset Printing Allow Default Clause.
to deactivate the second behavior, and
Unset Printing Factorizable Match Patterns.
to deactivate the first behavior (deactivating the first one
deactivates also the second one).
E.g. printing
match x with Eq => 1 | _ => 0 end
gives
match x with
| Eq => 1
| _ => 0
end
or (with default clause deactivates):
match x with
| Eq => 1
| Lt | Gt => 0
end
More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
|
| | | | | |
| | | | |
| | | | |
| | | | | |
This is to have a better symmetry between CCases and GCases.
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |/ / /
| | |
| | |
| | | |
And some code simplification.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|_|/ /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
| | |_|/ /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | | |
They were not used anymore since the previous patches.
|
| |\ \ \ \
| |/ / /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
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].
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- 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.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
| |\ \ \
| | | |
| | | |
| | | | |
functionalization.
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
#3125)
|
| | |_|_|_|_|/
|/| | | | | |
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |\ \ \ \ |
|
| | | |/ /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This function returns InProp or InSet for inductive types only when
the inductive type has been explicitly truncated to Prop or
(impredicative) Set.
For instance, singleton inductive types and small (predicative)
inductive types are not truncated and hence in Type.
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| |_|_|/ /
|/| | | | |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |/ / / |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ / |
|
| |/
|
|
|
|
|
| |
We generalize the possible use of levels to raw and glob printers.
This is potentially useful for printing ltac expressions which are the
glob level.
|
| |\ |
|
Enrico Tassi
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Théo Zimmermann
Pierre-Marie Pédrot
Gaëtan Gilbert
Matthieu Sozeau