| Age | Commit message (Expand) | Author |
| 2002-02-19 | Le type des evars transformees en meta n'etait pas normalise, et des Evars | barras |
| 2002-02-18 | bug #134: on appelait solve_simple_eqn avec une evar qui etait resolue | barras |
| 2002-02-15 | petits changements cosmetiques sur les tactiques | barras |
| 2002-02-14 | - Reforme de la gestion des args recursifs (via arbres reguliers) | barras |
| 2002-02-12 | petite modif pour ne pas expanser trop de let pendant l'unification | barras |
| 2002-02-11 | substitution et pattern modulo let | barras |
| 2002-02-07 | petit nettoyage de kernel/inductive | barras |
| 2002-02-04 | exceptionmal ratrappee | barras |
| 2002-01-31 | changement generation de schema d'elimination, False_rec est primitif, Constr... | mohring |
| 2002-01-25 | Correction bug 'Check [b]if b then O else O' | herbelin |
| 2002-01-24 | code mort | herbelin |
| 2002-01-24 | Réparation bug 'known_dependent' | herbelin |
| 2002-01-21 | warning en mode verbeux seulement | filliatr |
| 2002-01-18 | Le chargement des coercions est nécessaire même si le module n'est pas ouvert | herbelin |
| 2002-01-17 | Amélioration affichage échec lookup_eliminator | herbelin |
| 2002-01-16 | Correction d'un problème avec les motifs anonymes dépendant dans des argume... | herbelin |
| 2002-01-15 | Correction de de Bruijn incorrect pour le cas de dépendances vers l'avant | herbelin |
| 2001-12-20 | Non dépliage des Fix non réductibles dans Hnf | herbelin |
| 2001-12-19 | Insertion unification non seulement en tête mais à l'intérieur des motifs ... | herbelin |
| 2001-12-18 | Grossière erreur de typage | herbelin |
| 2001-12-18 | Nettoyage exceptions liées au vieux Case | herbelin |
| 2001-12-18 | Nettoyage exceptions liées au vieux Case; réparation du try with UserError ... | herbelin |
| 2001-12-13 | Contournement du problème des evars de type, typées par défaut dans Type (... | herbelin |
| 2001-12-13 | Contournement du problème des evars de type, typées par défaut dans Type | herbelin |
| 2001-12-13 | compat ocaml 3.03 | filliatr |
| 2001-12-11 | Mise en place de coercion dans les motifs | herbelin |
| 2001-11-29 | nouvel algo de conversion plus uniforme | barras |
| 2001-11-22 | La mise en forme normale du prédicat d'élimination était un peu trop viole... | herbelin |
| 2001-11-21 | Quelques autres petits problèmes résolus... | herbelin |
| 2001-11-21 | Simplification de la propagation du prédicat, bugs, et messages d'erreurs | herbelin |
| 2001-11-21 | Solution partielle au problème des alias dépendants pour les rendre compati... | herbelin |
| 2001-11-21 | Prise en compte des coercions pour typer les branches lorsqu'il y a une contr... | herbelin |
| 2001-11-20 | Ajout make_arity_signature | herbelin |
| 2001-11-20 | Correction bug contrainte de valeur trop restrictive sur le typage du type du... | herbelin |
| 2001-11-20 | Bug mauvaise instance | herbelin |
| 2001-11-20 | Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant | herbelin |
| 2001-11-19 | Bug nommage des fonctions définies par récursion mutuelle | herbelin |
| 2001-11-19 | Re-installation de l'affichage des globaux par des noms courts | herbelin |
| 2001-11-19 | Remise en place du Cast pour Correctness | herbelin |
| 2001-11-17 | User Casts are for helping pretyping, experimentally not to be kept | herbelin |
| 2001-11-12 | Suites modifs du noyau. Univ devient purement fonctionnel. | barras |
| 2001-11-09 | Nettoyage coercions et classes | herbelin |
| 2001-11-09 | code mort | herbelin |
| 2001-11-08 | Introduction d'univers frais dans les types implicites engendrés par le pré... | herbelin |
| 2001-11-08 | Rétablissement de la persistance des Cast; typage des LetIn sans recours à ... | herbelin |
| 2001-11-06 | corrections mineures suite au commit de restructuration du noyau | barras |
| 2001-11-06 | Suppression des local_constraints, des ctxtty et du focus. | clrenard |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-30 | Reorganisation de Goption. Passage des options l'utilisant en synchrone | letouzey |
| 2001-10-29 | Amérioration message d'erreur en cas d'échec du filtrage de premier ordre | herbelin |