Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Strengthening some of the results in ChoiceFacts.v. | 2017-03-03 | |
| | | | | | | | | | Further highlighting when the correspondence between variants of choice is independent of the domain and codomain of the function, as was done already done in the beginning of the file (suggestion from Jason). Adding some corollaries. | ||
* | Adding explicitly a file to work in the context of propositional extensionality. | 2017-03-03 | |
| | |||
* | Adding a file providing extensional choice (i.e. choice over setoids). | 2017-03-03 | |
| | | | | Also integrating suggestions from Théo. | ||
* | Adding various properties and characterization of the extensional | 2017-03-03 | |
| | | | | | | | axiom of choice (i.e. choice on setoids) and of the axiom selecting representatives in classes of equivalence. Also integrating suggestions from Théo. | ||
* | Slightly unifying renaming in ChoiceFacts.v. | 2017-03-03 | |
| | |||
* | Logic library: Adding a characterization of excluded-middle in term of | 2017-03-03 | |
| | | | | | | | | | | choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo). | ||
* | Formatting references with surrounding brackets in Diaconescu.v. | 2017-03-03 | |
| | |||
* | Fix a typo in Hurkens.v comment | 2016-12-19 | |
| | |||
* | Merge branch 'v8.6' | 2016-11-18 | |
|\ | |||
| * | Remove v62 from stdlib. | 2016-10-24 | |
| | | | | | | | | | | This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore. | ||
* | | Merge branch 'v8.6' | 2016-10-08 | |
|\| | |||
| * | Fixing unexpected "noise" introduced in commit 24d5448c. | 2016-10-06 | |
| | | | | | | | | A file was introduced by mistake in theories/Logic. | ||
* | | Merge branch 'v8.6' | 2016-10-05 | |
|\| | |||
| * | More tests for tactic "subst". | 2016-10-02 | |
| | | |||
* | | extensionality: Handle dependently-used hypotheses | 2016-09-19 | |
| | | |||
* | | Adding an "extensionality in H" tactic which applies functional | 2016-09-19 | |
|/ | | | | | | | | extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples. | ||
* | Typo in a comment of stdlib. | 2016-07-08 | |
| | |||
* | Moving the Tauto tactic to proper Ltac. | 2016-02-22 | |
| | | | | | | This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there. | ||
* | Merge branch 'v8.5' | 2016-01-29 | |
|\ | |||
| * | Fix bug #4503: mixing universe polymorphic and monomorphic | 2016-01-23 | |
| | | | | | | | | variables and definitions in sections is unsupported. | ||
* | | Merge branch 'v8.5' | 2016-01-21 | |
|\| | |||
| * | Update copyright headers. | 2016-01-20 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-12-17 | |
|\| | |||
| * | Refine tactic now shelves unifiable holes. | 2015-12-15 | |
| | | | | | | | | | | | | The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet. | ||
* | | Merge branch 'v8.5' | 2015-12-11 | |
|\| | |||
| * | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | 2015-12-10 | |
| | | | | | | | | Marking it as experimental. | ||
* | | Fix to previous commit (ClassicalFacts.v). | 2015-12-05 | |
| | | |||
* | | Adding proofs on the relation between excluded-middle and minimization. | 2015-12-05 | |
| | | | | | | | | | | | | | | In particular, a proof of the equivalence of excluded-middle and an unrestricted principle of minimization. Credits to Arnaud Spiwack for the ideas and formalizations of the proofs. | ||
* | | Merge branch 'v8.5' | 2015-11-29 | |
|\| | |||
| * | Univs: entirely disallow instantiation of polymorphic constants with | 2015-11-27 | |
| | | | | | | | | | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere. | ||
* | | Adding an amazing property of Prop. | 2015-11-07 | |
|/ | |||
* | Minor modifications to WeakFanTheorem. | 2015-09-08 | |
| | |||
* | Remove some outdated files and fix permissions. | 2015-07-31 | |
| | |||
* | Update headers. | 2015-01-12 | |
| | |||
* | Added an arithmetical characterization of the hypothesis of WKL. | 2014-12-01 | |
| | |||
* | Improving elimination with indices, getting rid of intrusive residual | 2014-11-02 | |
| | | | | local definitions... | ||
* | Make sure that Logic/ExtensionalityFacts gets compiled. | 2014-10-27 | |
| | |||
* | Fix some typos. | 2014-10-27 | |
| | |||
* | Fix some typos in comments. | 2014-10-27 | |
| | |||
* | EqdepFacts: generalize statements which were wrongly restricted to Prop. | 2014-10-22 | |
| | |||
* | ConstructiveEpsilon: simplify the before_witness type using non-uniform ↵ | 2014-10-16 | |
| | | | | parameters. | ||
* | Hurkens.v: Fix a syntax error. | 2014-09-26 | |
| | | | Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176. | ||
* | ClassicalFacts: adds a proof that weak excluded middle implies weak proof ↵ | 2014-09-26 | |
| | | | | | irrelevance. Application of previous commit in Hurkens.v. | ||
* | Hurkens.v: new paradox: type of modal propositions is not a retract. | 2014-09-26 | |
| | | | In particular there is no retract of the type of negative propositions in a negative proposition. | ||
* | Hurkens.v: fix coqdoc formatting in a comment. | 2014-09-26 | |
| | |||
* | Hurkens.v: update comments. | 2014-09-25 | |
| | |||
* | Return a Prop not an arbitrary Type, and correct a typo. | 2014-09-24 | |
| | |||
* | Hurkens.v: show proofs in coqdoc. | 2014-09-24 | |
| | |||
* | Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}]. | 2014-09-24 | |
| | |||
* | Hurkens.v: coqdoc documentation. | 2014-09-24 | |
| |