aboutsummaryrefslogtreecommitdiff
path: root/pretyping/clenv.ml
AgeCommit message (Expand)Author
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
2007-02-22Ajout fonction clenv_conv_leq pour résoudre les pbs de la formeherbelin
2007-02-21Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESherbelin
2006-11-19Dépendance inutile en Tacexpr, de proofs, qui se compile en principe aprèsherbelin
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
2006-10-25Suite commit 9277herbelin
2006-10-25Correction d'une tentative incorrecte (révision 9266) de clarificationherbelin
2006-10-24Ajout de la tactique "apply in".herbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau