| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-02-18 | Standardisation of function names about global references (especially, renami... | herbelin |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
| 2004-08-24 | Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi... | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-07-11 | Eta-expansion du predicat dans build_indrec (suite) | herbelin |
| 2004-07-11 | Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_... | herbelin |
| 2003-09-12 | Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in... | herbelin |
| 2003-09-09 | Ajout construction If primitive dans constr_expr et rawconstr | herbelin |
| 2003-09-06 | Paramétrisation vis à vis de existential_key | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-04-16 | simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis... | letouzey |
| 2003-03-12 | *** empty log message *** | barras |
| 2003-01-15 | Bug en présence de let-in | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-11-05 | Intégration des modifs de la branche mowgli : | herbelin |
| 2002-09-24 | Un peu (plus) d'ordre dans Nametab... | coq |
| 2002-08-13 | Renoncement à distinguer les types "constr" et "types"; nettoyage | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-02-14 | - Reforme de la gestion des args recursifs (via arbres reguliers) | barras |
| 2002-02-07 | petit nettoyage de kernel/inductive | barras |
| 2002-01-31 | changement generation de schema d'elimination, False_rec est primitif, Constr... | mohring |
| 2002-01-24 | code mort | herbelin |
| 2002-01-21 | warning en mode verbeux seulement | filliatr |
| 2002-01-17 | Amélioration affichage échec lookup_eliminator | herbelin |
| 2001-12-13 | compat ocaml 3.03 | filliatr |
