| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-02 | Better error message when found more than once object of name ... | Pierre Boutillier |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-08-22 | Nicer code concerning dirpaths and modpath around Lib | letouzey |
| 2013-08-22 | Misc changes around coqtop.ml : | letouzey |
| 2013-08-22 | Less "Coq" strings everywhere | letouzey |
| 2013-08-08 | Side effect free implementation of admit (Isabelle's oracle) | gareuselesinge |
| 2013-06-02 | Modest protection against "injection" and co raising anomaly in | herbelin |
| 2013-03-12 | Hipattern : consider jmeq only when Logic.JMeq is loaded | letouzey |
| 2013-02-27 | Coqlib: minor simplifications | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-18 | use List.rev_map whenever possible | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-25 | Monomorphization (interp) | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 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 |
