| Age | Commit message (Expand) | Author |
| 2010-03-07 | Fix treatment of remaining unification constraints: raise a more | msozeau |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-02 | Continuing r12485-12486 and r12549 (cleaning around name generation) | herbelin |
| 2009-12-01 | Continuing r12485-12486 (cleaning around name generation) | herbelin |
| 2009-11-12 | Backtrack on fixing #2167 | herbelin |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-11-11 | Redoing broken commit r12498 (fixing bug #2167 + attempt to test the | herbelin |
| 2009-11-11 | Fixing bug #2167 + attempt to test the compatibility of a more robust | herbelin |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-10-30 | Attempt to capture on time unification errors for "with" bindings. | herbelin |
| 2009-09-18 | - Fixed a bug in checking that implicit arguments are all correctly | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-06-02 | Backtrack on experimental unification with sort variables: it requires | msozeau |
| 2009-05-23 | A try at using sort variables during unification. Instead of refreshing | msozeau |
| 2009-05-10 | - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it | herbelin |
| 2009-04-08 | Some dead code removal + cleanups | letouzey |
| 2009-04-08 | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin |
| 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-10-26 | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-06-18 | Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk | herbelin |
| 2008-04-27 | - Backtrack sur option with_types suite à confusion sur l'utilisation | herbelin |
| 2008-04-26 | - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec | herbelin |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-15 | Mises à jour bugs, CHANGES, code mort | herbelin |
| 2008-04-14 | Diverses corrections | herbelin |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-04-04 | Protection de rewrite in contre le dépliage des constantes dans w_unify, ce qui | herbelin |
| 2008-03-19 | Do another pass on the typeclasses code. Correct globalization of class | msozeau |
| 2008-02-09 | Solde de code mort et petites optimisations sur lesquels je suis | herbelin |
| 2008-02-07 | Mise en place d'une toute petite amélioration de l'unification de | herbelin |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-10-12 | - Préservation des appels récursifs de tête dans ltac (réponse au "wish" | herbelin |
| 2007-10-12 | Uniformisation du comportement de rewrite et rewrite in : quand le | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-09-28 | Correction bug 1711 | herbelin |
| 2007-06-06 | Toujours l'unification de apply : nouveau raffinement pour ne tester | herbelin |
| 2007-05-29 | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin |
| 2007-05-28 | Contrôle de la compatibilité de apply via une information dans les | herbelin |
| 2007-05-24 | Unification suite: petits affinements pour préserver la compatibilité | herbelin |
| 2007-05-23 | Tentative d'insertion de coercions avant unification si le type de la | herbelin |
| 2007-05-23 | Suite restructuration unification et division des problèmes | herbelin |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-21 | Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-04-18 | - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771 | herbelin |