aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.ml
Commit message (Expand)AuthorAge
* Noise for nothingGravatar pboutill2012-03-02
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...Gravatar herbelin2011-07-16
* Fixing discriminate for identity.Gravatar herbelin2011-05-26
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
* Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"Gravatar letouzey2011-01-31
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Fix bug 2307Gravatar pboutill2010-05-20
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* Add a flag to control rewriting under lambdas. Otherwise makes someGravatar msozeau2008-03-20
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
* dead codeGravatar letouzey2007-07-11
* Addition of a "Combined Scheme" vernacular command for building the conjuncti...Gravatar msozeau2006-12-23
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Ajout nat_path et find_referenceGravatar herbelin2006-02-04
* exporting the global reference to the inductive " \/ " in coqlib andGravatar bertot2006-01-25
* Ajout booléens; nettoyageGravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* Branchement EmptyT, UnitT, IT vers leur equivalent dans SetGravatar herbelin2004-03-11
* Extension de zarithGravatar herbelin2003-11-04
* Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...Gravatar herbelin2003-11-01
* Optimisation de gen_constant_in_modulesGravatar herbelin2003-10-21
* identityT = identityGravatar herbelin2003-10-14
* identity est equivalent sur Type (sauf sans argument)Gravatar herbelin2003-10-10
* Un peu plus de souplesse dans la globalisation des noms utilises par les tact...Gravatar herbelin2003-09-26
* open superfluGravatar herbelin2003-09-12
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* Mise en place d'un traducteur de noms v7->v8Gravatar herbelin2003-03-31
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14