| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \
| | |
| | |
| | | |
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
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | |/
| |/| |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
| | | |
| | |
| | |
| | |
| | | |
`internal_ghost` was an artifact to ease porting of the ml4 rules. Now
that the location is optional we can finally get rid of it.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| | | |
| | |
| | |
| | | |
Now it is a private field, locations are optional.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| | |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
Maxime Dénès
Hugo Herbelin
Emilio Jesus Gallego Arias
Amin Timany
Pierre-Marie Pédrot
Pierre Letouzey
Théo Zimmermann
Jason Gross
Gaetan Gilbert