aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2008-03-29Fix test-suite files, change conflicting notation "->rel" and the othersmsozeau
2008-03-28Improve error handling and messages for typeclasses. msozeau
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-27Various fixes on typeclasses:msozeau
2008-03-21Correct bug introduced in r10589, where we lost information thatmsozeau
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-03-17Add the possibility of specifying constants to unfold for typeclassmsozeau
2008-03-17* Factorizing code : context_chop was used in several files (even as chop_con...vsiles
2008-03-16Using the "relation" constant made some unifications fail in the newmsozeau
2008-03-15Application de refresh_universes dans typing.ml et retyping.ml : lesherbelin
2008-03-11Typo commit 10653herbelin
2008-03-10Pas très propre de reposer sur la capture des anomalies (et celaherbelin
2008-03-10fold travaille maintenant sur la forme beta-iota-zeta réduite duherbelin
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