Backport PRs to branch v8.10 #9963
Merged
Conversation
This file contains 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
vbgl
changed the title
vbgl
force-pushed
the
staging-v8.10
branch
2 times, most recently
from
006a02b
to
bb5719d
Compare
ejgallego
reviewed
May 2, 2019
vbgl
force-pushed
the
staging-v8.10
branch
6 times, most recently
from
67f1c0a
to
5c6322d
Compare
vbgl
force-pushed
the
staging-v8.10
branch
2 times, most recently
from
e4eaef5
to
a43025c
Compare
This comment has been minimized.
This comment has been minimized.
vbgl
force-pushed
the
staging-v8.10
branch
5 times, most recently
from
30638cf
to
48926a2
Compare
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
vbgl
added a commit
to vbgl/coq
that referenced
this pull request
Jul 12, 2019
vbgl
force-pushed
the
staging-v8.10
branch
3 times, most recently
from
1c65a4b
to
06a3c6e
Compare
…coq#10956) This should fix the issue when creating new session panes. The initial session panes, however, might still be wrongly sized, as we do not yet know, at the time they are created, if the window manager will respect the user settings fixing the window size. (cherry picked from commit 882e37c)
…tual window size. (Fixes coq#10956)
Only the deprecated one was documentated, and the deprecation was not mentioned. (cherry picked from commit f71733e)
(cherry picked from commit 6423932)
Rels that exist inside the environment at the time of the closure creation are fetched in the global environment, while we only use the local list of relevance for FRels. All the infrastructure was implicitly relying on this kind of behaviour before the introduction of SProp. Fixes coq#11150: pattern is 10x slower in Coq 8.10.0 (cherry picked from commit b8b835c)
… efficient way.
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> (cherry picked from commit 73bb54d)
(cherry picked from commit 7e082e5)
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes coq#10504. (cherry picked from commit a5d124d)
and do not run template_candidate in the upper layers when the template attribute is given. This means we can use an over-approximation in the upper layer implementation of template_candidate (returning false even in cases which the kernel may accept) if we ever want to. (cherry picked from commit 1db8720)
…ly and nonlinear universes
…ion regression). (cherry picked from commit 597a8a0)
…q#11090 (coercion+notation regression)
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.
This is #9961, that has been automatically closed by mistake…