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.
When the hypothesis contained
a @ (b @ c)
where the implicit arguments toconcat
did not match the implicit arguments inferred for@concat _ _ _ _ a (@concat _ _ _ _ b c)
(according topattern
),left_associate_concat_in
looped, repeatedly findinga @ (b @ c)
, and failing to associate it to the left, introducing constant transports that did nothing.This is now fixed, by picking up and passing the implicit arguments, explicitly.
The comment in Modalities/ReflectiveSubuniverse.v has been updated; a naive use of
rewrite@A
causes the subsequent rewrite to fail. I haven't tracked it down, but I suspect @mikeshulman wouldn't have much trouble updating the file.This fixes #744; the test is now added to Tests.v.