| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
[coq] Adapt to coq/coq#9815
|
|
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)
|
|
overlay for PR 9733
|
|
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.
|
|
See https://gitlab.com/coq/coq/-/jobs/187496964
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
chronological order.
|
|
skip_pattern
Reviewed-by: ppedrot
|
|
(warn if bar is a nonprimitive projection)
|
|
Reviewed-by: jashug
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
[dune] Full Dune support.
|
|
This is a fairly small cleanup on the `vernac_interp` function, which
makes code cleaner and for example would allow to have `Load` inside
`Load`. [Not that we would ever want that]
|
|
This is the right thing to do until we refine the program architecture
a bit to use EConstr.
Closes #9163 .
|
|
|
|
|
|
|
|
|
|
|
