PR for branch legacy #150
Draft
PR for branch legacy #150
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
require Coq 8.14 later in opam and CI due to CoqPrime
* fix an inconsistent section numbering * small correction in latex document * small correction in latex document * implicit arguments for impHn (to do: iffH, existH, andH, etc.) * implicit arguments for notH (to do: iffH, existH, andH, etc.) * implicit arguments for forallH (to do: iffH, existH, andH, etc.) * implicit arguments for orH (to do: iffH, existH, andH, etc.) * implicit arguments for andH (to do: iffH, existH, etc.) * implicit arguments for iffH (to do: existH, etc.) * implicit arguments for equal (to do: existH, etc.) * implicit arguments for existH (to do: apply, var,atomic, etc.) * implicit arguments for var (to do: apply, atomic, etc.) * implicit arguments for atomic (to do: apply, Tcons, etc.) * implicit arguments for apply (to do: Tcons, etc.) * implicit arguments for ifThenElse (to do: Tcons, etc.) * implicit arguments for Tnil (to do: Tcons, etc.) * implicit arguments for Tcons * implicit arguments for Tcons * minor changes * Update theories/ordinals/Ackermann/Deduction.v Co-authored-by: Karl Palmskog <[email protected]> * Update theories/ordinals/MoreAck/FOL_notations.v Co-authored-by: Karl Palmskog <[email protected]> * Local changes to implicit arguments (partial) * switch to regular Coq dev Docker in ci due to MathComp dev currently not getting rebuilt * remove useless 'fol.' prefixes * remove a lot of useless 'fol.' prefixes for abstract syntax constructors --------- Co-authored-by: Karl Palmskog <[email protected]>
* Make Require commands more explicit (with From) * Add From to Requires * Fix a deprecation error The suggested replacement of N.div_le_mono with N.Div0.le_mono caused an error in versions < 8.17
remove a bunch of deprecate warnings
* small corrections * corrections to the general introduction * corrections to the general introduction * corrections chapter 2
* buggy * minor change * Removed useless variants of functions canon and Canon
* minor change * Data type associated with an ordinal notation is now a coercio
* minor change * small changes in doc
* minor change * small changes in doc * simplify the proposition 'alpha < phi0 beta' * simplify the proposition 'alpha < phi0 beta' * improve Alectryon output * minor changes in pdf doc * minor changes in pdf doc
* minor change * small changes in doc * simplify the proposition 'alpha < phi0 beta' * simplify the proposition 'alpha < phi0 beta' * improve Alectryon output * minor changes in pdf doc * minor changes in pdf doc
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.
No description provided.