aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Specif.v
Commit message (Expand)AuthorAge
...
* Some lemmas about dependent choice + extensions of Compare_dec +Gravatar herbelin2009-11-16
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* Une passe sur les réels:Gravatar herbelin2008-03-23
* Ajout exist & cie à la table des hints par symétrie avec ex_intro &Gravatar herbelin2007-06-22
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* DocumentationGravatar herbelin2005-05-19
* Nouvelle en-têteGravatar herbelin2004-07-16
* sumbool et sumor affich avec 'if' si possibleGravatar herbelin2004-04-06
* Décomposition automatique des règles d'analyse syntaxique pour lesGravatar herbelin2004-02-12
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Passage des notations de type dans type_scopeGravatar herbelin2003-10-28
* CommentairesGravatar herbelin2003-10-23
* Argument de except, error implicite seulement en v8; Changement 'as notation'...Gravatar herbelin2003-10-14
* Argument implicite pour None, error, exceptGravatar herbelin2003-10-13
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...Gravatar herbelin2003-09-23
* Concentration des notations officielles dans Init/Notations; restructuration ...Gravatar herbelin2003-05-21
* Activation des implicites pour la v8Gravatar herbelin2003-04-09
* Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesGravatar herbelin2002-11-26
* Retablissement SynDef Value/ErrorGravatar herbelin2002-11-25
* Généralisation de l'utilisation de NotationGravatar herbelin2002-11-24
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* changement generation de schema d'elimination, False_rec est primitif, Constr...Gravatar mohring2002-01-31
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
* Suppression d'Export redondantsGravatar herbelin2001-11-14
* and_rec redondantGravatar letouzey2001-09-27
* Fin de la modif Exc/optionGravatar mohring2001-08-30
* ajout option , Exc --> option, et lemmes dans les theoriesGravatar mohring2001-08-29
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* documentation automatique de la bibliothèque standardGravatar filliatr2001-04-11
* Introduction d'une preuve de False_recGravatar mohring2001-03-30
* entetesGravatar filliatr2001-03-15
* fichiers prelude CoqGravatar filliatr1999-12-13