| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-05-08 | Uniformizing the [if_warn] flag used for warning printing and put | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-02-18 | use List.rev_map whenever possible | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-19 | Array.create is deprecated | pboutill |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | 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-04 | Replacing some str with strbrk | 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-12-17 | A pass on warning printings. Made systematic the use of msg_warning so | herbelin |
| 2011-10-11 | Various simplifications about constant_of_delta and mind_of_delta | letouzey |
| 2010-11-08 | Refresh universes in params when generating schemes (Closes: #2429) | glondu |
| 2010-09-28 | Remove some occurrences of "open Termops" | glondu |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-18 | Applicative commutative cuts in Fixpoint guard condition | pboutill |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 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-08-23 | A new kind of automatically generated scheme "congr" for equality types | herbelin |
| 2009-08-11 | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-02-06 | pushed evar reduction in kernel | barras |
| 2008-12-28 | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin |
| 2008-11-09 | - Fixed bug 1968 (inversion failing due to a Not_found bug introduced in | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-06 | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack |
| 2007-05-17 | Nettoyage et standardisation des messages d'erreurs. | herbelin |
| 2007-03-15 | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin |
| 2006-12-12 | Correction du bug #1273, deuxième version (avec des shémas d'elimination pl... | notin |
| 2006-12-12 | Correction du bug #1273 (problème avec les paramètres non récursivement un... | notin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2005-12-17 | Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ... | herbelin |
| 2005-12-17 | Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-28 | parametres inductifs | mohring |
