Fixing Generate OrderedType and removing warnings #8
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
These tactics stopped working around the time of v8.7 and in particular they are used by the Generate OrderedType vernacular.
Simply generates an OrderedType instance for ascii and string, to make sure we notice if the vernacular and underlying tactics stop working again.
This was broken in ff28f8b and so the generation of ordered types for mutually inductive types had no chance of working anymore.
…tives Again, the behaviour of some apply/eapply of eq_lt/eq_gt changed (which I do not understand) and must be worked around. Added a test for Generate OrderedType with a pair of mutually inductive definitions so that somthing breaks next time it stops working.
Usage of destruct 0, induction 0 and inversion_clear 0 has become deprecated.
This was referenced Feb 25, 2019
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Mainly fixing the Generate OrderedType vernacular which had been broken since v8.7 as far as I know. I think it's one of the main feature of the contrib in terms of usability.
This branch fixes it both for inductive types and mutually inductive types; a test file has been added with a couple of calls to the vernacular.
It also fixes some deprecation warnings both in the tactic's ML code and in proof scripts, there should be none remaining anymore.