aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-11-21*** empty log message ***herbelin
2001-11-21MAJherbelin
2001-11-21Amélioration messages d'erreur arité incorrecte (notamment record)herbelin
2001-11-21Possibilité d'appeler check avec l'option -byteherbelin
2001-11-21Simplification de la propagation du prédicat, bugs, et messages d'erreursherbelin
2001-11-21documentation de mes actions recentes sur les theories (PL)letouzey
2001-11-21remise au gout du jour du repertoire theories/Sorting de la V6.3letouzey
2001-11-21remise au gout du jour du repertoire theories/Sorting de la V6.3letouzey
2001-11-21La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...herbelin
2001-11-21Solution partielle au problème des alias dépendants pour les rendre compati...herbelin
2001-11-21Prise en compte des '?' aussi dans le type des définitionsherbelin
2001-11-21Oubli des contraintes d'univers lors de la suppression des cast dans un commi...herbelin
2001-11-21Make sure that NatRing won't loop forever.bertot
2001-11-21Un bug dans le scriptherbelin
2001-11-21Sur l'exahustivité du filtrageherbelin
2001-11-21Sur la cumulativité dans les tactiquesherbelin
2001-11-21Nouveaux exemplesherbelin
2001-11-21Prise en compte des coercions pour typer les branches lorsqu'il y a une contr...herbelin
2001-11-20Ajout isEvarherbelin
2001-11-20Ajout make_arity_signatureherbelin
2001-11-20Ajout mkArityherbelin
2001-11-20hack temporaire concernant les remarks/modulesletouzey
2001-11-20iota généraliséletouzey
2001-11-20*** empty log message ***herbelin
2001-11-20Correction bug contrainte de valeur trop restrictive sur le typage du type du...herbelin
2001-11-20types vs constrherbelin
2001-11-20Bug mauvaise instanceherbelin
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
2001-11-20types vs constrherbelin
2001-11-20Cosmétique avant toutherbelin
2001-11-20Suppression des Cast externes dans les définitionsherbelin
2001-11-20Code mortherbelin
2001-11-20Ajout quelques fonctions; code mortherbelin
2001-11-19Bug nommage des fonctions définies par récursion mutuelleherbelin
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
2001-11-19Mise en place d'une méthode directe pour indiquer le type des déclarations ...herbelin
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
2001-11-19Renommage qualid_of_global en shortest_qualid_of_globalherbelin
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-16MAJherbelin
2001-11-16*** empty log message ***herbelin
2001-11-15Ajout d'un fichier Max dans Arith, et enrichissement du Min.letouzey
2001-11-15Ajout des fonctions tail-recursives tail_plus et tail_mult.letouzey
2001-11-14Une liste plus precise des .v a prendre en compte pour les dependances, a l'e...herbelin
2001-11-14oubli: changement de nil en nilTmayero
2001-11-14Changement de list en listT, cons en consT et app en appTmayero
2001-11-14Suppression d'Export redondantsherbelin
2001-11-14Revolution culturelle: suppression des arguments propletouzey