aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Datatypes.v
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* CompSpec2Type is used to build functions, it should be Defined, not QedGravatar letouzey2010-02-13
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* Datatypes.length and app defined back via fun+fix instead of FixpointGravatar letouzey2009-11-06
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Fine-tuning rewriting from "eq_true b": using <- to rewrite true to bGravatar herbelin2008-11-23
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
* Déplacement des opérations sur bool dans l'état initialGravatar herbelin2007-04-28
* Mise en forme des theoriesGravatar notin2006-10-17
* Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiésGravatar herbelin2006-05-29
* - 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
* Added option_mapGravatar herbelin2005-03-31
* Nouvelle en-têteGravatar herbelin2004-07-16
* Definition de la notation de la paire par un motif recursifGravatar herbelin2004-03-17
* Duplication temporaire des règles de syntaxe des pairesGravatar herbelin2003-12-16
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Ajout lemme projectionsGravatar herbelin2003-11-12
* Passage de la notations de paire dans core_scopeGravatar herbelin2003-10-28
* ajoutsGravatar herbelin2003-10-21
* Des implicites plus 'naturels' pour eq_ind, identity_ind and coGravatar herbelin2003-10-17
* Argument de None implicite seulement en v8Gravatar herbelin2003-10-14
* Argument implicite pour None, error, exceptGravatar herbelin2003-10-13
* identity est equivalent sur Type (sauf sans argument)Gravatar herbelin2003-10-10
* Delimiters N devient 'nat'Gravatar herbelin2003-10-10
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
* NettoyageGravatar herbelin2003-09-21
* Bind et Delimit pour natGravatar herbelin2003-09-12
* Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...Gravatar herbelin2003-09-11
* Concentration des notations officielles dans Init/Notations; restructuration ...Gravatar herbelin2003-05-21
* Intégration DatatypesSyntax à DatatypesGravatar herbelin2003-04-17
* Activation des implicites pour la v8Gravatar herbelin2003-04-09
* Généralisation de l'utilisation de NotationGravatar herbelin2002-11-24
* DocGravatar herbelin2002-02-22
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 19:51:12 +0000