aboutsummaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...herbelin
2011-05-26Fixing discriminate for identity.herbelin
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2011-01-31Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"letouzey
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-05-20Fix bug 2307pboutill
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-03Added "etransitivity".herbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-01-01Switched to "standardized" names for the properties of eq andherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
2008-03-20Add a flag to control rewriting under lambdas. Otherwise makes somemsozeau
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
2007-07-11dead codeletouzey
2006-12-23Addition of a "Combined Scheme" vernacular command for building the conjuncti...msozeau
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-04-07- Documentation of the Program tactics.msozeau
2006-02-04Ajout nat_path et find_referenceherbelin
2006-01-25exporting the global reference to the inductive " \/ " in coqlib andbertot
2005-12-30Ajout booléens; nettoyageherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
2004-07-16Nouvelle en-têteherbelin
2004-03-11Branchement EmptyT, UnitT, IT vers leur equivalent dans Setherbelin
2003-11-04Extension de zarithherbelin
2003-11-01Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...herbelin
2003-10-21Optimisation de gen_constant_in_modulesherbelin
2003-10-14identityT = identityherbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-09-26Un peu plus de souplesse dans la globalisation des noms utilises par les tact...herbelin
2003-09-12open superfluherbelin
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
2003-05-19Restructuration des procédures de filtrageherbelin
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea