aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
Commit message (Expand)AuthorAge
* Reorganize comment documentation of ChoiceFacts.vGravatar Gaetan Gilbert2017-05-03
* Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
* Fixing missing PropFacts.v in Logic/vo.itarget.Gravatar Hugo Herbelin2017-03-28
* Merge PR#392: strengthened the statement of JMeq_eq_depGravatar Maxime Dénès2017-03-24
|\
* | Add a forgotten (?) line to "theories/Logic/vo.itarget".Gravatar Matej Kosik2017-03-19
* | Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoGravatar Maxime Dénès2017-03-14
|\ \
* | | Strengthening some of the results in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
* | | Adding explicitly a file to work in the context of propositional extensionality.Gravatar Hugo Herbelin2017-03-03
* | | Adding a file providing extensional choice (i.e. choice over setoids).Gravatar Hugo Herbelin2017-03-03
* | | Adding various properties and characterization of the extensionalGravatar Hugo Herbelin2017-03-03
* | | Slightly unifying renaming in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
* | | Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
* | | Formatting references with surrounding brackets in Diaconescu.v.Gravatar Hugo Herbelin2017-03-03
| * | Simplifying the proof of NoRetractToModalProposition.paradox inGravatar Hugo Herbelin2017-02-24
|/ /
* | Fix a typo in Hurkens.v commentGravatar Jason Gross2016-12-19
| * strengthened the statement of JMeq_eq_depGravatar Abhishek Anand2016-12-11
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\
| * Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\|
| * Fixing unexpected "noise" introduced in commit 24d5448c.Gravatar Hugo Herbelin2016-10-06
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * More tests for tactic "subst".Gravatar Hugo Herbelin2016-10-02
* | extensionality: Handle dependently-used hypothesesGravatar Jason Gross2016-09-19
* | Adding an "extensionality in H" tactic which applies functionalGravatar Hugo Herbelin2016-09-19
|/
* Typo in a comment of stdlib.Gravatar Hugo Herbelin2016-07-08
* Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\|
| * Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* | Fix to previous commit (ClassicalFacts.v).Gravatar Hugo Herbelin2015-12-05
* | Adding proofs on the relation between excluded-middle and minimization.Gravatar Hugo Herbelin2015-12-05
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* | Adding an amazing property of Prop.Gravatar Hugo Herbelin2015-11-07
|/
* Minor modifications to WeakFanTheorem.Gravatar Hugo Herbelin2015-09-08
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Update headers.Gravatar Maxime Dénès2015-01-12
* Added an arithmetical characterization of the hypothesis of WKL.Gravatar Hugo Herbelin2014-12-01
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
* ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Gravatar Arnaud Spiwack2014-10-16
* Hurkens.v: Fix a syntax error.Gravatar Arnaud Spiwack2014-09-26