aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/EqdepFacts.v
Commit message (Expand)AuthorAge
* Typo in a comment of stdlib.Gravatar Hugo Herbelin2016-07-08
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
* Return a Prop not an arbitrary Type, and correct a typo.Gravatar Matthieu Sozeau2014-09-24
* 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
* Some basics facts about eq_dep.Gravatar Hugo Herbelin2014-07-15
* - 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
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Identities over types satisfying Uniqueness of Identity ProofsGravatar herbelin2012-12-04
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
* More lemmas relating the different equivalent formulations of eq_dep.Gravatar herbelin2011-07-16
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* - Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.Gravatar herbelin2008-06-10
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
* Passage de Set à Type dans Relations et WellfoundedGravatar herbelin2007-02-06
* Correction typo eq_rec_eq (cf bug #1339)Gravatar herbelin2007-01-31
* Mise en forme des theoriesGravatar notin2006-10-17
* Réajout de eq_rec_eq oublié lors de la modularisation de EqdepGravatar herbelin2006-03-30
* Modularisation des preuves concernant la logique classique, l'indiscernabilit...Gravatar herbelin2006-03-05