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 patch removes the old/basic meet and makes the new/advanced meet the only and default meet algorithm.
The configuration options (
-flambda2-basic-meet
,-flambda2-advanced-meet
, and theflambda2-meet-algorithm
OCAMLPARAM) are kept to avoid breaking scripts, but are now silently ignored.Note that theChanged this because it makes more sense to use different names in #3538.Meet_and_join_new
module is NOT renamed toMeet_and_join
, and theMeet_and_join
module simply forwards toMeet_and_join_new
. This is intentional in order to re-use the same dispatch mechanism for the new join algorithm in #3538.Meet_and_join_new
is now renamed toMeet_and_join
.This PR also takes the opportunity to clean up the interfaces:
meet_env_extension
;join
from theFlambda2_types
interface