| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
4.02.3 has been the minimal OCaml version for a while now.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
"_something")
|
| | | |
| | |
| | |
| | |
| | | |
This includes _ and insecable space which can be used in idents and
this allows more precise heuristics.
|
| | |/
|/| |
|
| |\ \
| | |
| | |
| | | |
3e70ea9c.
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |/ /
| |
| |
| |
| | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
Unfortunately, some manual synchronization is needed between the
constr parser and the table of constr/pattern levels.
We do this synchronization which was missing in the commit moving
"x -> y" to a user-level notation.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
```
|
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Gaëtan Gilbert
Matthieu Sozeau
Amin Timany
Pierre Letouzey
Théo Zimmermann
Jason Gross