aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
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
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-03Cleaning a little bit the files talking about descriptions: avoidingherbelin
2011-10-05Removing vernacular code mistakenly committed.herbelin
2011-08-23Use of the standard terminology for Diaconescu's theorem (not "paradox").herbelin
2011-08-10Less ambitious application of a notation for eq_rect. We proposedherbelin
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
2011-07-16Some facts about functional extensionality (especially alternativeherbelin
2011-07-16More lemmas relating the different equivalent formulations of eq_dep.herbelin
2010-12-10First release of Vector library.pboutill
2010-10-23Used multiple lists of implicit arguments to transfer the choices ofherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 23:07:08 +0000