aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2001-12-19Insertion unification non seulement en tête mais à l'intérieur des motifs ...herbelin
2001-12-18Grossière erreur de typageherbelin
2001-12-18Nettoyage exceptions liées au vieux Caseherbelin
2001-12-18Nettoyage exceptions liées au vieux Case; réparation du try with UserError ...herbelin
2001-12-13Contournement du problème des evars de type, typées par défaut dans Type (...herbelin
2001-12-13Contournement du problème des evars de type, typées par défaut dans Typeherbelin
2001-12-13compat ocaml 3.03filliatr
2001-12-11Mise en place de coercion dans les motifsherbelin
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-22La mise en forme normale du prédicat d'élimination était un peu trop viole...herbelin
2001-11-21Quelques autres petits problèmes résolus...herbelin
2001-11-21Simplification de la propagation du prédicat, bugs, et messages d'erreursherbelin
2001-11-21Solution partielle au problème des alias dépendants pour les rendre compati...herbelin
2001-11-21Prise en compte des coercions pour typer les branches lorsqu'il y a une contr...herbelin
2001-11-20Ajout make_arity_signatureherbelin
2001-11-20Correction bug contrainte de valeur trop restrictive sur le typage du type du...herbelin
2001-11-20Bug mauvaise instanceherbelin
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
2001-11-19Bug nommage des fonctions définies par récursion mutuelleherbelin
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
2001-11-19Remise en place du Cast pour Correctnessherbelin
2001-11-17User Casts are for helping pretyping, experimentally not to be keptherbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-09Nettoyage coercions et classesherbelin
2001-11-09code mortherbelin
2001-11-08Introduction d'univers frais dans les types implicites engendrés par le pré...herbelin
2001-11-08Rétablissement de la persistance des Cast; typage des LetIn sans recours à ...herbelin
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
2001-10-30Reorganisation de Goption. Passage des options l'utilisant en synchroneletouzey
2001-10-29Amérioration message d'erreur en cas d'échec du filtrage de premier ordreherbelin
2001-10-16Nettoyage Recordobj et conséquencesherbelin
2001-10-15Insertion automatique des motifs de let-in s'il ne sont pas explicitement men...herbelin
2001-10-15Rustine pour rendre les messages d'erreurs de la compilation des Cases plus l...herbelin
2001-10-15Insertion automatique des motifs de let-in s'il ne sont pas explicitement men...herbelin
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-03Bug de synthèse du prédicat en présence d'arguments non filtrable; correct...herbelin
2001-10-03Bug d'affichage du prédicat, bug d'affichage des clauses en présence de dé...herbelin
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
2001-09-21Réparation des options Set Printing and coherbelin
2001-09-20Transparentbarras
2001-09-20Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même q...herbelin
2001-09-19Blindage, de peur que des types entrant non en forme normale ne provoque des ...herbelin
2001-09-19Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...herbelin
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...herbelin
2001-09-19Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ...herbelin
2001-09-14Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)herbelin
2001-09-14L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...herbelin