aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-10-06Fixing unexpected "noise" introduced in commit 24d5448c.Hugo Herbelin
2016-10-02More tests for tactic "subst".Hugo Herbelin
2016-07-08Typo in a comment of stdlib.Hugo Herbelin
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-05Fix to previous commit (ClassicalFacts.v).Hugo Herbelin
2015-12-05Adding proofs on the relation between excluded-middle and minimization.Hugo Herbelin
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-07Adding an amazing property of Prop.Hugo Herbelin
2015-09-08Minor modifications to WeakFanTheorem.Hugo Herbelin
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-12-01Added an arithmetical characterization of the hypothesis of WKL.Hugo Herbelin
2014-11-02Improving elimination with indices, getting rid of intrusive residualHugo Herbelin
2014-10-27Make sure that Logic/ExtensionalityFacts gets compiled.Guillaume Melquiond
2014-10-27Fix some typos.Guillaume Melquiond
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-22EqdepFacts: generalize statements which were wrongly restricted to Prop.Arnaud Spiwack
2014-10-16ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Arnaud Spiwack
2014-09-26Hurkens.v: Fix a syntax error.Arnaud Spiwack
2014-09-26ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...Arnaud Spiwack
2014-09-26Hurkens.v: new paradox: type of modal propositions is not a retract.Arnaud Spiwack
2014-09-26Hurkens.v: fix coqdoc formatting in a comment.Arnaud Spiwack
2014-09-25Hurkens.v: update comments.Arnaud Spiwack
2014-09-24Return a Prop not an arbitrary Type, and correct a typo.Matthieu Sozeau
2014-09-24Hurkens.v: show proofs in coqdoc.Arnaud Spiwack
2014-09-24Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Arnaud Spiwack
2014-09-24Hurkens.v: coqdoc documentation.Arnaud Spiwack
2014-09-24A new version of Hurkens.v.Arnaud Spiwack
2014-08-26Prove forall extensionalityJason Gross
2014-08-26sed s'/_one_var/_on/g'Jason Gross
2014-08-26Generalize EqdepFactsJason Gross
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-07-17Completing c236b51348d2 by fixing EqdepFactsv actually committing theHugo Herbelin
2014-07-15Added a (constructive) proof of Weak Konig's lemma for decidable trees.Hugo Herbelin
2014-07-15Some basics facts about eq_dep.Hugo Herbelin
2014-06-26Remove some theories that have been deprecated for 10 years.Guillaume Melquiond
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 17:08:05 +0000