aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
Commit message (Expand)AuthorAge
* 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
* ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: new paradox: type of modal propositions is not a retract.Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: fix coqdoc formatting in a comment.Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: update comments.Gravatar Arnaud Spiwack2014-09-25
* Return a Prop not an arbitrary Type, and correct a typo.Gravatar Matthieu Sozeau2014-09-24
* Hurkens.v: show proofs in coqdoc.Gravatar Arnaud Spiwack2014-09-24
* Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Gravatar Arnaud Spiwack2014-09-24
* Hurkens.v: coqdoc documentation.Gravatar Arnaud Spiwack2014-09-24
* A new version of Hurkens.v.Gravatar Arnaud Spiwack2014-09-24
* Prove forall extensionalityGravatar Jason Gross2014-08-26
* sed s'/_one_var/_on/g'Gravatar Jason Gross2014-08-26
* Generalize EqdepFactsGravatar Jason Gross2014-08-26
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Completing c236b51348d2 by fixing EqdepFactsv actually committing theGravatar Hugo Herbelin2014-07-17
* Added a (constructive) proof of Weak Konig's lemma for decidable trees.Gravatar Hugo Herbelin2014-07-15
* Some basics facts about eq_dep.Gravatar Hugo Herbelin2014-07-15
* Remove some theories that have been deprecated for 10 years.Gravatar Guillaume Melquiond2014-06-26
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Closing bug #3164Gravatar Julien Forest2014-04-04
* fixup complement FinGravatar Pierre Boutillier2014-02-24
* FinFun.v: results about injective/surjective/bijective fonctions over finite ...Gravatar Pierre Letouzey2014-02-07
* Generalize eq_proofs_unicityGravatar Jason Gross2013-12-12
* Improved the presentation of the proof of UIP_refl_nat.Gravatar Hugo Herbelin2013-12-04
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
* A constructive proof of Fan theorem where paths are represented by predicates.Gravatar herbelin2013-06-02
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Making subset_eq_compat applying over more general domain "Type" (see #2938).Gravatar herbelin2012-12-05
* Identities over types satisfying Uniqueness of Identity ProofsGravatar herbelin2012-12-04
* Isolating the ingredients of the proof of Prop<>Type (r15973). SeeingGravatar herbelin2012-11-15
* Added a proof that Prop<>Type, for arbitrary fixed Type.Gravatar herbelin2012-11-15
* A decidability property of functional relations over decidable codomains.Gravatar herbelin2012-11-15
* For the record, two examples of short proofs of uniqueness of identityGravatar herbelin2012-11-15
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15