| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Fixes #9840
|
|
It is important to fully normalize the term, *including inductive
parameters of constructors*; see https://github.com/coq/coq/issues/9840
for details on what goes wrong if this does not happen, e.g., from using
the vm rather than cbv.
Supersedes / closes #9655
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
Ack-by: proux01
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: jashug
|
|
|
|
Something like "("; [ s = SELF -> { s } ]; ")" in a GRAMMAR EXTEND in
a mlg file was causing an error message such as
OCAMLOPT f.ml
File "f.mlg", line 179, characters 55-67: # not in a semantic rule so line doesn't match anything in the mlg file
Error: This expression has type ('a, Extend.mayrec, 'a) Extend.symbol
but an expression was expected of type
('a, Extend.norec, 'b) Extend.symbol
Type Extend.mayrec is not compatible with type Extend.norec
It is now
COQPP f.mlg
Error: 'SELF' or 'NEXT' illegal in anonymous entry level
|
|
Instead of just string (and empty strings for tokens without payload)
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
warn if [bar] nonprimitive projection.
Reviewed-by: ppedrot
|
|
This reverts commit 1eb8b9dc3ff0e464c9cd6c7f12a1c9db4fa57423.
This commit is no longer necessary
|
|
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8. We hereby assume that all file paths are valid UTF-8.
We also now actually test both python2 and python3 on the CI.
|
|
|
|
This should fix #9705
I'm kind-of cargo-cult coding here, from things like
https://docs.python.org/3/library/sys.html#sys.displayhook and
https://github.com/coq/coq/issues/9705#issuecomment-471996313, but
hopefully this fixes the issue without breaking anything. (I am really
a novice when it comes to the str/bytes distinction in python3.)
|
|
|
|
|
|
One can now register a quotation using a grammar rule with
QUOTATION("name:"). "name:" becomes a keyword and the token is
generated for name: followed by a an identifier or a parenthesized
text. Eg
constr:x
string:[....]
ltac:(....)
ltac:{....}
The delimiter is made of 1 or more occurrences of the same parenthesis,
eg ((.....)) or [[[[....]]]]. The idea being that if the text happens to
contain the closing delimiter, one can make the delimiter longer and avoid
confusion (no escaping). Eg
string:[[ .. ']' .. ]]
Nesting the delimiter is allowed, eg ((..((...))..)) is OK.
The text inside the quotation is returned as a string (including the
parentheses), so that a third party parser can take care of it.
Keywords don't need to end in ':'.
|
|
Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals
Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t
Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
|
|
|
|
Reviewed-by: ppedrot
|
|
skip_pattern
Reviewed-by: ppedrot
|
|
(warn if bar is a nonprimitive projection)
|
|
Reviewed-by: jashug
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Ack-by: gares
|
|
I thought the test-suite infrastructure was always passing
`-async-proofs-cache force`, but in fact it does it only for interactive
tests.
This should speed up the tests quite a bit.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.
|
|
Reviewed-by: gares
|
|
The quoting was incorrect thus scripts didn't properly work.
|
|
Once we have the good `plugins/ltac/dune` in place for bootstrapping,
we should not regenerate it. Thanks to @maximedenes for the report.
This fixes `make states` always rebuilding ltac's dependencies.
|
|
There's never a proof available in ocamldebug
I don't know about Drop.
|
|
Fix #9845
|
|
only.
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
|
|
Reviewed-by: Zimmi48
|
|
|
|
This is convenient for the bootstrap of `coqdep`
|
