| Age | Commit message (Expand) | Author |
| 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 |
| 2001-10-16 | Nettoyage Recordobj et conséquences | herbelin |
| 2001-10-15 | Insertion automatique des motifs de let-in s'il ne sont pas explicitement men... | herbelin |
| 2001-10-15 | Rustine pour rendre les messages d'erreurs de la compilation des Cases plus l... | herbelin |
| 2001-10-15 | Insertion automatique des motifs de let-in s'il ne sont pas explicitement men... | herbelin |
| 2001-10-11 | Suppression option immediate_discharge; nettoyage de Declare et conséquences | herbelin |
| 2001-10-09 | Suppression des arguments sur les constantes, inductifs et constructeurs | barras |
| 2001-10-03 | Bug de synthèse du prédicat en présence d'arguments non filtrable; correct... | herbelin |
| 2001-10-03 | Bug d'affichage du prédicat, bug d'affichage des clauses en présence de dé... | herbelin |
| 2001-10-02 | Ajout de dynamiques pour les quotations constr et tactic | delahaye |
| 2001-09-21 | Réparation des options Set Printing and co | herbelin |
| 2001-09-20 | Transparent | barras |
| 2001-09-20 | Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même q... | herbelin |
| 2001-09-19 | Blindage, de peur que des types entrant non en forme normale ne provoque des ... | herbelin |
| 2001-09-19 | Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit... | herbelin |
| 2001-09-19 | Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de... | herbelin |
| 2001-09-19 | Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ... | herbelin |
| 2001-09-14 | Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local) | herbelin |
| 2001-09-14 | L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã... | herbelin |