aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
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
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-04Closing bug #3164Julien Forest
2014-02-24fixup complement FinPierre Boutillier
2014-02-07FinFun.v: results about injective/surjective/bijective fonctions over finite ...Pierre Letouzey
2013-12-12Generalize eq_proofs_unicityJason Gross
2013-12-04Improved the presentation of the proof of UIP_refl_nat.Hugo Herbelin
2013-08-02Adding a dependent version of equal_f, thus fixing #3074.ppedrot
2013-06-02A constructive proof of Fan theorem where paths are represented by predicates.herbelin
2013-01-18Unset Asymmetric Patternspboutill
2012-12-05Making subset_eq_compat applying over more general domain "Type" (see #2938).herbelin
2012-12-04Identities over types satisfying Uniqueness of Identity Proofsherbelin
2012-11-15Isolating the ingredients of the proof of Prop<>Type (r15973). Seeingherbelin
2012-11-15Added a proof that Prop<>Type, for arbitrary fixed Type.herbelin
2012-11-15A decidability property of functional relations over decidable codomains.herbelin
2012-11-15For the record, two examples of short proofs of uniqueness of identityherbelin
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-05 01:02:51 +0000