aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Logic.v
Commit message (Expand)AuthorAge
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* modification de la definition des def inductives unitaires et autorisation d'...Gravatar mohring2002-01-29
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
* Suppression d'Export redondantsGravatar herbelin2001-11-14
* TransparentGravatar barras2001-09-20
* ajout option , Exc --> option, et lemmes dans les theoriesGravatar mohring2001-08-29
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* entetesGravatar filliatr2001-03-15
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* fichiers prelude CoqGravatar filliatr1999-12-13