| Age | Commit message (Expand) | Author |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-07-16 | Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and... | herbelin |
| 2011-05-26 | Fixing discriminate for identity. | herbelin |
| 2011-05-05 | Definitions of positive, N, Z moved in Numbers/BinNums.v | letouzey |
| 2011-01-31 | Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar" | letouzey |
| 2010-11-02 | Move stuff about positive into a distinct PArith subdir | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-30 | Move [delayed] to util and use [force_delayed] everywhere to force | msozeau |
| 2010-06-12 | Fixing spelling: pr_coma -> pr_comma | herbelin |
| 2010-05-20 | Fix bug 2307 | pboutill |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-08-03 | Added "etransitivity". | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-01-01 | Switched to "standardized" names for the properties of eq and | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-05-28 | Notation concise pour la valeur par défaut des cas reconnus comme | herbelin |
| 2008-03-20 | Add a flag to control rewriting under lambdas. Otherwise makes some | msozeau |
| 2007-10-05 | Added the automatic generation of the boolean equality if possible and the | vsiles |
| 2007-07-11 | dead code | letouzey |
| 2006-12-23 | Addition 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-04 | Ajout nat_path et find_reference | herbelin |
| 2006-01-25 | exporting the global reference to the inductive " \/ " in coqlib and | bertot |
| 2005-12-30 | Ajout booléens; nettoyage | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-02-18 | Standardisation of function names about global references (especially, renami... | herbelin |
| 2005-02-06 | Nettoyage et documentation de Library | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-11 | Branchement EmptyT, UnitT, IT vers leur equivalent dans Set | herbelin |
| 2003-11-04 | Extension de zarith | herbelin |
| 2003-11-01 | Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ... | herbelin |
| 2003-10-21 | Optimisation de gen_constant_in_modules | herbelin |
| 2003-10-14 | identityT = identity | herbelin |
| 2003-10-10 | identity est equivalent sur Type (sauf sans argument) | herbelin |
| 2003-09-26 | Un peu plus de souplesse dans la globalisation des noms utilises par les tact... | herbelin |
| 2003-09-12 | open superflu | herbelin |
| 2003-06-10 | Déplacement traducteur de nom dans Constrextern pour accès aux noms longs | herbelin |
| 2003-05-19 | Restructuration des procédures de filtrage | herbelin |
| 2003-03-31 | Mise en place d'un traducteur de noms v7->v8 | herbelin |
| 2003-03-31 | factorisation des "constant" dans les contrib/* ( maintenant dans coqlib ) | corbinea |