| Age | Commit message (Expand) | Author |
|---|
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-09-18 | Cleaning interface of Util. | 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-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-02 | "Let in" in pattern hell, one more iteration | pboutill |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-03-01 | Univ: a univ_depends function to avoid a hack in Inductiveops | letouzey |
| 2012-01-16 | Inductiveops.nb_*{,_env} cleaning | pboutill |
| 2010-12-18 | Univ.constraints made fully abstract instead of being a Set of abstract stuff | 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-05-18 | Applicative commutative cuts in Fixpoint guard condition | pboutill |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-03-12 | fixed confusion between number of cstr arguments and number of pattern variab... | barras |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | 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-13 | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin |
| 2009-08-11 | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin |
| 2009-08-02 | Improved parameterization of Coq: | herbelin |
| 2009-07-15 | - Fixing bug #2139 (kernel-based test of well-formation of elimination | herbelin |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-10-07 | fixing r11433 again: | barras |
| 2008-07-25 | Correction d'une incohérence de typage des inductifs polymorphes: les | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2007-09-06 | Itération sur les sous-termes dans la vérification de la condition de garde | herbelin |
| 2007-08-09 | Modification de control_only_guard, qui utilise maintenant | notin |
| 2007-03-15 | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |
| 2006-10-01 | Ajout allowed_sorts | herbelin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-04-27 | - Distinction explicite des parties paramètres et arguments dans le type | herbelin |
| 2006-03-22 | - Correction bug calcul mind_consnrealargs, introduit à la révision | herbelin |
| 2006-02-07 | oubli de code de debugging | herbelin |
| 2006-01-30 | Fonctions retournant les arits des constructeurs et inductifs (suite) | herbelin |
| 2006-01-30 | Fonctions retournant les arits des constructeurs et inductifs | herbelin |
| 2006-01-10 | Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 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 | Moving subst_inductive from tacinterp to inductiveops for better for reuse in... | herbelin |
| 2005-01-14 | Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed | sacerdot |
| 2004-12-29 | Bug control_only_guard | herbelin |
| 2004-12-06 | Commentaire | herbelin |
| 2004-08-24 | Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc... | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-11-18 | Ajout mis_constructor_nargs_env | herbelin |
