| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
| |
One less global flag.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\
| |
| |
| | |
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.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| | |
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
| |/
|
|
|
|
|
|
|
| |
Together with #1122, this makes `VernacInstance` the only command in
the Coq codebase that cannot be statically determined to open a proof.
The reasoning for the commands moved to `VtSideff` is that
parser-altering commands should be always marked `VtNow`; the rest can
be usually marked as `VtLater`.
|
| |
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | |
| |
| |
| |
| | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| | |/
|/|
| |
| | |
We do up to `Term` which is the main bulk of the changes.
|
| | |
| |
| |
| | |
Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
|
| |/
|
|
|
|
| |
This makes sense here as the main client is `Stdargs`. This helps with
the concerns @herbelin had in
https://github.com/coq/coq/issues/6008#issuecomment-341107793
|
| |
|
|
|
| |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
| |
|
|
|
|
|
|
|
| |
We interpret meta-commands directly, instead of going by an
intermediate "classifier step".
The code could still use some further refactoring, in particular, the
`part_of_script` bit is a bit strange likely coming from some special
treatment of `VtMeta` in the `query` call, and should go away.
|
| |
|
|
|
|
|
|
|
|
| |
The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.
We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| |\
| |
| |
| | |
top of the linking chain.
|
| | |
| |
| |
| |
| | |
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
| |/
|
|
| |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
| |
|
|
|
|
|
| |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
| |\ |
|
| | |
| |
| |
| |
| | |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
| |/
|
|
|
|
|
|
|
| |
Since camlp5 parses from left, the last ", z" was parsed as part of an
arbitrary long list of "x1 , .. , xn" and a syntax error was raised
since an extra ", z" was still expected.
We support this by translating "x , .. , y , z" into "x , y , .. , z"
and reassembling the arguments appropriately after parsing.
|
| | |
|
| |
|
|
|
| |
`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This string contains the base-10 representation of the number (big endian)
Note that some inner parsing stuff still uses bigints, see egramcoq.ml
|
| | | | |
|
| | | | |
|
| | |/
| |
| |
| |
| | |
The command has been broken for 15 years. It is basically dead code.
Its former behavior can be mimicked with Set Printing Implicit. Show.
|
Théo Zimmermann
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Matthieu Sozeau
Gaëtan Gilbert
Pierre-Marie Pédrot
Amin Timany
Pierre Letouzey