| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
#9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
|
|
and to not use the VM
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
|
|
Fixes #9844
|
|
|
|
|
|
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
|
|
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
|
|
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.
|
