| Age | Commit message (Collapse) | Author |
|---|
|
This could still use some more work due to the way proofs are
structured, in particular:
- the handling of the primary type w.r.t. Econstr
- refining Info.t so open/close invariants hold by typing
Very interestingly, better typing means that the tension between
tension between `start_dependent_lemma` and the handling of mutual
definitions starts to surface.
In particular, the information contained in `Info.thms` is not to be
used by all non-standard terminators.
However, it seems that such refactoring would better fit once we have
finished cleaning up the regular save path.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
|
|
|
|
We clean the hack bypassing the interpretation of "'pat" in binders
and move it to comDefinition.ml. In particular, we fix the exact
subterm to which Eval has to apply in the hack, and remove the
artificial cast we had introduced.
|
|
|
|
If we need more fine-tuning we should manage the warnings with the
standard Coq mechanism.
|
|
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
|
|
We remove Coq's wrapper over gramlib's grammar constructors.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
The current API does just exist as a workaround for a bug.
|
|
Steps towards unification with `DeclareDef` API.
|
|
Steps towards unification with `DeclareDef` API.
|
|
We move `Recthm` to `DeclareDef` so it is shared by interactive and
direct fixpoint declaration.
This is the last step before unifying both paths.
|
|
Note that we had to introduce a `restrict_ucontext` parameter to be
faithful to the implementation in obligations, however this looks like
a bug.
|
|
|
|
|
|
|
|
First commit of a series that will unify (and enforce) the handling of
mutual constants. We will split this in several commits as to easy
debugging / bisect in case of problems.
In this first commit, we move the actual declare logic to a common
place.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
Obligations/Program currently allocates a libobject object just to
check that there are no obligations pending at the end of a section.
I think this is not the right use case for libobject, thus we turn the
check into an explicit one at the vernac level.
|
|
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Warning: in notations, the name "bigint" actually meant "bignat". A
clarification will eventually be needed.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
There is a lot of check overhead in the code, we will try to provide a
more convenient API for manipulation of remaining obligations.
|
|
Both the interactive and non-interactive save path share some internal
table update code.
|
|
We make internal types `private` as an step towards the unification of
the save path with the rest of the system.
In particular, this is allow us to guarantee invariants
w.r.t. external users as the large majority of fields are always
constant.
This will also enable at some point a common creation of proof entry
with the rest of the system.
|
|
|
|
|
|
|
|
|
|
|
|
After we moved `start_lemma_com` to `vernacentries` the comment on
`start_lemma_with_initialization` needs update.
|
|
It should be safe now after previous refactoring in lemmas.
|
|
This is a step towards cleanup of the `start` lemma path.
|
|
We instead favor the `build_by_tactic` function which should at some
point better integrated in the declare core.
|
|
In anticipation for more consolidation of duplicated functionality.
|
|
Most of the parameters were named, we fix the remaining cases.
|
|
Unfortunately, we cannot go further and parse Export as a legacy
attribute because this syntax conflicts with the Export command.
|
|
- Legacy attributes can now be specified in any order.
- Legacy attribute Cumulative maps to universes(cumulative).
- Legacy attribute NonCumulative maps to universes(noncumulative).
- Legacy attribute Private maps to private(matching).
We use "private(matching)" and not "private(match)" because we cannot
use keywords within attributes.
|
|
Ack-by: herbelin
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
