aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/EqdepFacts.v
Commit message (Expand)AuthorAge
* 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