aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
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
2010-07-22Backported r13308 (ConstructiveEpsilon.v) to branch v8.3herbelin
2010-07-22Update of ConstructiveEpsilon.v by Jean-François Monin.herbelin
2010-06-09Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in amsozeau
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-05-28Generalized the formulation of classic_set in propositional contextsherbelin
2010-05-22Added UIP_dec on suggestion of Eelis on #coq irc.herbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-30Small improvements around coqdoc (including fix for bug #2288)herbelin
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-11-24Small extra result on JMeq vs eq_dep.herbelin
2009-11-16Some lemmas about dependent choice + extensions of Compare_dec +herbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-11 09:23:38 +0000