aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2008-01-30Debug 0-ary typeclasses support, use new redefinition support for default tacticmsozeau
2008-01-21Correction du bug #1754notin
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...msozeau
2008-01-18bug in accessing n-th abstractionbarras
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...msozeau
2008-01-05Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...msozeau
2008-01-02Better resolution of implicit parameters in typeclass binders, add extensiona...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-10-12- Préservation des appels récursifs de tête dans ltac (réponse au "wish"herbelin
2007-10-12Uniformisation du comportement de rewrite et rewrite in : quand leherbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-10-01Amendement à la révision 10124 : déplacement de apprec_nohdbeta entreherbelin
2007-09-28Correction bug 1711herbelin
2007-09-26Complément aux commits 10124 et 10125 sur l'inférence de type (correction herbelin
2007-09-25Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.herbelin
2007-09-21Petit complément au commit 10131.herbelin
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
2007-09-18Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)herbelin
2007-09-17Raffinement de l'algorithme d'inférence de typeherbelin
2007-09-16Réponse à une incompatibilité introduite dans 10114 (calcul du nombreherbelin
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
2007-09-06Itération sur les sous-termes dans la vérification de la condition de gardeherbelin
2007-09-04Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesherbelin
2007-09-01Suite commit 10103 (expansion des défs locales triviales dans l'étapeherbelin
2007-08-29Prise en compte des redéfinitions de variables (définitions localesherbelin
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
2007-08-25Extension et documentation de real_clean/evar_define dans evarutil.ml:herbelin
2007-08-10- Correction d'un bug de de Bruijn dans abstract_predicate (lié auherbelin
2007-08-09Modification de control_only_guard, qui utilise maintenantnotin
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
2007-06-30Correction bug sur factorisation affichage paramètres (cf r9918)herbelin
2007-06-30Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Recordherbelin
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
2007-06-09Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...msozeau
2007-06-07Unification des types + clause filtrage manquante + uniformisation localeherbelin
2007-06-06Toujours l'unification de apply : nouveau raffinement pour ne testerherbelin
2007-06-05Amélioration de la complexité de auto (l'utilisation des types dansherbelin
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
2007-05-24Unification suite: petits affinements pour préserver la compatibilitéherbelin
2007-05-23Tentative d'insertion de coercions avant unification si le type de laherbelin
2007-05-23Suite restructuration unification et division des problèmesherbelin
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin