aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Wf.v
AgeCommit message (Expand)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-09-28well_founded_induction de nouveau transparentletouzey
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-07-08recursion bien fondee sur des pairsfilliatr
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2003-04-28Un principe light d'elimination de Acc, suivant les remarques de Yves Bertotletouzey
2003-04-09Activation des implicites pour la v8herbelin
2003-03-12*** empty log message ***barras
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-02-19Uniformisation des theoremes dans Set et Type (def. de Acc_rect etbarras
2002-02-14option -dump-glob pour coqdocfilliatr
2002-01-09MAJ des Id pour coqwebherbelin
2001-11-14Suppression d'Export redondantsherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-03-15entetesfilliatr
1999-12-13fichiers prelude Coqfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 06:09:38 +0000