-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Port coq-plugin-lib to Coq 8.11 #42
Draft
InnovativeInventor
wants to merge
42
commits into
master
Choose a base branch
from
8.11
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Changes from 41 commits
Commits
Show all changes
42 commits
Select commit
Hold shift + click to select a range
763990a
Port plibrary.ml4 to mlg
InnovativeInventor cf1ab43
Add missing cases to map3
InnovativeInventor 5ebea67
Update Global.body_of_constant call to reflect changes in Coq impl
InnovativeInventor 3ab41c8
Port to 8.10; handle all cases; remove unused Environ
InnovativeInventor d9f5ca6
Fail loudly in map3 if args have mismatched size
InnovativeInventor 7ede24e
Add Globnames to scope
InnovativeInventor a3dd7f9
Port defutils to Coq 8.11; whew!
InnovativeInventor ad7c8e6
Remove unused import from nameutils
InnovativeInventor f90d9fa
Port inference.ml to 8.11; remove unused imports
InnovativeInventor bad58f6
Finish porting over contextutils.ml (breaking change!)
InnovativeInventor c69de0d
Turn "pattern-matching is not exhaustive" warnings back to warnings
InnovativeInventor 0fcf2c8
Remove unused import
InnovativeInventor 827ea2f
Remove unused import
InnovativeInventor 5e92a93
Add necessary import
InnovativeInventor 6f7a0dd
Add warning 40 to not fatal list of warnings
InnovativeInventor 391a7d7
Update KerName.make2 calls to Names.KerName.make
InnovativeInventor ba601dd
Finish porting substitution.ml to 8.11 (breaking change!)
InnovativeInventor 343c23f
Exclude more warnings from turning into errors
InnovativeInventor 3eeea21
Port more logicutils
InnovativeInventor a7c7ae1
Port modutils
InnovativeInventor cd43754
Partial port of transform.ml and transform.mli
InnovativeInventor 6d2b009
Finish porting transform
InnovativeInventor fad8b1e
Port devutils/printing
InnovativeInventor c425423
Turn more warnings back to warnings
InnovativeInventor 53b15cd
Port decompiler
InnovativeInventor 36c0ba0
Fix invalid forward reference issue by rearranging imports
InnovativeInventor 1e441c4
Remove unnecessary plibrary.ml build artifact
InnovativeInventor c249fd9
Switch definition ordering back to original to reduce PR diff
InnovativeInventor b555622
Remove Proof.compact call
InnovativeInventor 5d4e2e0
Fix declare_definition call
InnovativeInventor 9b8d5b0
Fix declare_definition bug
InnovativeInventor e582a0c
Add partial implementation of inductive type case
InnovativeInventor 89efa78
Add fixes
InnovativeInventor 3a59347
Attempt to fix list_elim bug
InnovativeInventor 0e9cb9b
Finish fixing list_elim bug; todo: refactor and clean up
InnovativeInventor 966f8d4
Comment out debugging statement
InnovativeInventor d76e4be
Add back missing type decl
InnovativeInventor 15132c6
Remove vim .swp file
InnovativeInventor eafd2c4
Silence more build warnings
InnovativeInventor 3630afd
Change types of api func
InnovativeInventor a4a353d
Fix forward ref issue
InnovativeInventor c8cdf42
Set allow_evars to true (bug fix)
InnovativeInventor File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -23,3 +23,4 @@ plugin/Makefile | |
| plugin/.merlin | ||
| *.out | ||
| _opam | ||
| src/plibrary.ml | ||
Oops, something went wrong.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I excluded this from git because it appears to be a build artifact that gets generated whenever
build.shis run.