| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|\ \
| | |
| | |
| | | |
from location in file
|
|\ \ \ |
|
| | | | |
|
| |/ /
| | |
| | |
| | |
| | | |
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.
|
| | |
| | |
| | |
| | | |
linking chain.
|
| |/
|/|
| |
| | |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
|/
|
|
|
|
|
| |
These hacks to warn the users about needed modules are not needed
anymore in 8.8, as the proper error message is done in 8.7 already.
This helps in avoiding a dependency from parsing to MlTop.
|
|\ |
|
|\ \
| | |
| | |
| | | |
restructuration
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
|\ \ \ |
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
| | |
| | |
| | |
| | |
| | | |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
| | | |
|
| |/
| |
| |
| |
| |
| |
| |
| |
| | |
`G_vernac` was depending on `toplevel` just for parsing the compat
number information. IMHO this was not the right place, so I have moved
the parsing bits to parsing and updated the files.
This allows to finally separate the `toplevel` from Coq, which avoids
linking it in alternative toplevels.
|
|/
|
|
|
|
|
|
|
| |
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 requires to change the status of Inductive (we have also changed
CoInductive and Variant) from keyword to identifier.
|
| |
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Since previous commit, some plugins are not loaded initially anymore :
extraction, funind. To ease this transition toward a mandatory Require,
we hack here the vernac grammar in order to get customized error messages
telling what to Require instead of the dreadful "Illegal begin of vernac".
Normally, these fake grammar entries are overloaded later by the grammar
extensions in these plugins. This code is meant to be removed in a few releases,
when this transition is considered finished.
NB : In a first attempt, a similar trick was tried in g_tactics.ml4 to
provide customized error message for "functional induction" and "functional
inversion", but this was leading to anomalies.
|
| | | |
|
| |/
|/|
| |
| |
| |
| | |
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.
|
|/
|
|
|
| |
Introduced for Proof-General but unused at the current time,
undocumented and can raise anomalies.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:
```
Goal Type.
⋮
Save id.
```
has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.
We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.
It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
|
| |
| |
| |
| | |
It has been deprecated for a while in favor of `Qed`.
|
| | |
|
| |
| |
| |
| | |
The addition to the test suite showcases the usage.
|
| |\ |
|
| |\ \
| | | |
| | | |
| | | | |
let-ins
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
| |/| |
|
| | | |
|