aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-03-06Toujours suite commits 10623 et 10624:herbelin
2008-03-06Suite commit 10623:herbelin
2008-03-06Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nherbelin
2008-03-05Correction d'une typo restant du commit 10557 et cause d'échec de contribsherbelin
2008-02-29Petite modif pour pouvoir faire "intros until 0" qui introduit autant aspiwack
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
2008-02-14Suspension de l'introduction de delta dans apply : certaines contribsherbelin
2008-02-14Added default canonical structures (see example in test-suite)corbinea
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
2008-02-13Correction de ce qui semble être un petit bug dans la gestion de laherbelin
2008-02-11Correction d'un bug de clearnotin
2008-02-10Fixing bug 1795 (occur check was not correctly done)herbelin
2008-02-09Solde de code mort et petites optimisations sur lesquels je suisherbelin
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
2008-02-08Move generally useful definition of nf_evar on contexts to evarutil.msozeau
2008-02-07Mise en place d'une toute petite amélioration de l'unification deherbelin
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
2008-01-31Finish let| implementation and document itmsozeau
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