aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Datatypes.v
AgeCommit message (Expand)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-12Ajout lemme projectionsherbelin
2003-10-28Passage de la notations de paire dans core_scopeherbelin
2003-10-21ajoutsherbelin
2003-10-17Des implicites plus 'naturels' pour eq_ind, identity_ind and coherbelin
2003-10-14Argument de None implicite seulement en v8herbelin
2003-10-13Argument implicite pour None, error, exceptherbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-10-10Delimiters N devient 'nat'herbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-21Nettoyageherbelin
2003-09-12Bind et Delimit pour natherbelin
2003-09-11Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...herbelin
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
2003-04-09Activation des implicites pour la v8herbelin
2002-11-24Généralisation de l'utilisation de Notationherbelin
2002-02-22Docherbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2002-01-09MAJ des Id pour coqwebherbelin
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-03-15entetesfilliatr
1999-12-13fichiers prelude Coqfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 06:03:55 +0000