Multiple payload types in tokens #9815
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
8 tasks
proux01
commented
Mar 22, 2019
ppedrot
reviewed
Mar 22, 2019
proux01
added a commit
to proux01/ltac2
that referenced
this pull request
Mar 24, 2019
4567139 to
3e05e50
Compare
|
To sum up
|
proux01
added a commit
to proux01/ltac2
that referenced
this pull request
Mar 29, 2019
proux01
added a commit
to proux01/ltac2
that referenced
this pull request
Mar 30, 2019
proux01
added a commit
to proux01/ltac2
that referenced
this pull request
Mar 30, 2019
ppedrot
reviewed
Mar 30, 2019
|
@proux01 Can you rebase this PR so that I merge it? |
Instead of just string (and empty strings for tokens without payload)
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
|
Rebased |
|
@ppedrot CI green |
ppedrot
approved these changes
Apr 1, 2019
ppedrot
added a commit
that referenced
this pull request
Apr 1, 2019
Reviewed-by: ppedrot Ack-by: proux01
ppedrot
added a commit
to rocq-prover/ltac2
that referenced
this pull request
Apr 1, 2019
[coq] Adapt to rocq-prover/rocq#9815
|
Thanks! |
maximedenes
pushed a commit
to maximedenes/coq
that referenced
this pull request
May 6, 2019
maximedenes
pushed a commit
to maximedenes/coq
that referenced
this pull request
May 6, 2019
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Instead of just string (and empty strings for tokens without payload)
This is mostly useless by itself but is used in #8764 and @ppedrot expressed a preference for and independent PR (#8764 (comment)).
It also takes the opportunity to remove most of the few Obj.magic left after #9548
This will conflict with #9733 I'll rebase here or offer a patch there, whichever comes first.