aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Logic.v
AgeCommit message (Expand)Author
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2002-11-24Généralisation de l'utilisation de Notationherbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2002-01-29modification de la definition des def inductives unitaires et autorisation d'...mohring
2002-01-09MAJ des Id pour coqwebherbelin
2001-11-14Suppression d'Export redondantsherbelin
2001-09-20Transparentbarras
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-03-15entetesfilliatr
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ...filliatr
1999-12-13fichiers prelude Coqfilliatr