| Age | Commit message (Expand) | Author |
| 2009-12-30 | Fixing bug #2193: computation of dependencies in the "match" return | herbelin |
| 2009-11-27 | Added support for definition of fixpoints using tactics. | herbelin |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-10-25 | Improved the treatment of Local/Global options (noneffective Local on | 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-11 | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-06-28 | Improve return predicate inference by making the return type dependent | msozeau |
| 2009-06-06 | Fixing bug #2106 ("match" compilation with multi-dependent constructor). | herbelin |
| 2009-04-08 | Some dead code removal + cleanups | letouzey |
| 2009-02-19 | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack |
| 2009-02-06 | pushed evar reduction in kernel | barras |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-11-27 | Fix (?) a pattern matching compilation problem: | msozeau |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-10 | - Correction bug 1841 (identificateurs incorrects avec Subclass) | herbelin |
| 2008-06-09 | - Correction de la version simplifiée (filtrage sur deux sig | herbelin |
| 2008-05-28 | Notation concise pour la valeur par défaut des cas reconnus comme | herbelin |
| 2008-05-05 | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin |
| 2008-04-01 | Finish enhancemenent of return clause inference from tycons, integrating | msozeau |
| 2008-03-29 | Fix test-suite files, change conflicting notation "->rel" and the others | msozeau |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-01-17 | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-09-25 | Suppression de tous les alias de la forme x:=x dans la compilation du filtrage. | herbelin |
| 2007-09-06 | Uniformisation politique de nommage evd/isevars (evd si evar_defs, | herbelin |
| 2007-08-10 | - Correction d'un bug de de Bruijn dans abstract_predicate (lié au | herbelin |
| 2007-03-15 | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin |
| 2006-11-22 | Code mort découvert par Matthieu | herbelin |
| 2006-10-05 | Correction de deux cas où les types inductifs n'étaient pas comparés | herbelin |
| 2006-09-23 | Correction d'un bug de coercion de pattern introduit dans la 8.1beta | herbelin |
| 2006-05-29 | The "clean integration of subtac" patch. | msozeau |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-04-28 | Typo dans précédent commit (8755); protection renforcée dans analyse claus... | herbelin |
| 2006-04-27 | - Distinction explicite des parties paramètres et arguments dans le type | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-04-25 | Code mort (suite) | herbelin |
| 2006-04-25 | Suppression code mort | herbelin |
| 2006-04-14 | Pas fier | herbelin |
| 2006-04-10 | Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous... | msozeau |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau |
| 2006-01-30 | Suppression fonctions d'interprétation du vieux Case | herbelin |
| 2006-01-30 | - Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer | herbelin |
| 2006-01-30 | - Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer; | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |