aboutsummaryrefslogtreecommitdiff
path: root/pretyping/clenv.ml
AgeCommit message (Expand)Author
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-02Continuing r12485-12486 and r12549 (cleaning around name generation)herbelin
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-12Backtrack on fixing #2167herbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-11-11Redoing broken commit r12498 (fixing bug #2167 + attempt to test theherbelin
2009-11-11Fixing bug #2167 + attempt to test the compatibility of a more robustherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-30Attempt to capture on time unification errors for "with" bindings.herbelin
2009-09-18- Fixed a bug in checking that implicit arguments are all correctlyherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-02Backtrack on experimental unification with sort variables: it requires msozeau
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
2009-05-10- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itherbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-06pushed evar reduction in kernelbarras
2008-10-26Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiherbelin
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-04-27- Backtrack sur option with_types suite à confusion sur l'utilisationherbelin
2008-04-26- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-15Mises à jour bugs, CHANGES, code mortherbelin
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-04Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiherbelin
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-02-09Solde de code mort et petites optimisations sur lesquels je suisherbelin
2008-02-07Mise en place d'une toute petite amélioration de l'unification deherbelin
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
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-09-28Correction bug 1711herbelin
2007-06-06Toujours l'unification de apply : nouveau raffinement pour ne testerherbelin
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
2007-05-21Essai d'une nouvelle heuristique pour clenv_unique_resolver : si leherbelin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-04-18- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771herbelin