aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Specif.v
AgeCommit message (Expand)Author
2009-11-16Some lemmas about dependent choice + extensions of Compare_dec +herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-05-12MAJ et bricoles diversesherbelin
2008-03-23Une passe sur les réels:herbelin
2007-06-22Ajout exist & cie à la table des hints par symétrie avec ex_intro &herbelin
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-03-17Modification des propriétés (svn:executable)notin
2005-05-19Documentationherbelin
2004-07-16Nouvelle en-têteherbelin
2004-04-06sumbool et sumor affich avec 'if' si possibleherbelin
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-10-28Passage des notations de type dans type_scopeherbelin
2003-10-23Commentairesherbelin
2003-10-14Argument de except, error implicite seulement en v8; Changement 'as notation'...herbelin
2003-10-13Argument implicite pour None, error, exceptherbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2003-04-09Activation des implicites pour la v8herbelin
2002-11-26Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesherbelin
2002-11-25Retablissement SynDef Value/Errorherbelin
2002-11-24Généralisation de l'utilisation de Notationherbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
2002-01-09MAJ des Id pour coqwebherbelin
2001-11-14Suppression d'Export redondantsherbelin
2001-09-27and_rec redondantletouzey
2001-08-30Fin de la modif Exc/optionmohring
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-03-30Introduction d'une preuve de False_recmohring
2001-03-15entetesfilliatr
1999-12-13fichiers prelude Coqfilliatr