aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Expand)Author
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-21In "progress", extending the set of evars w/o solving an existing one isherbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-02Reverted an incorrect code simplification in function status_changedherbelin
2009-10-30Take constraints into account in the "instantiate" tacticherbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Made unification patch 12268 even more ad hoc (if evars remain in aherbelin
2009-08-11Relatively ad hoc fix to an ill-typed instantiation bug in typeherbelin
2009-07-08Don't use recent ocaml tolerance for pattern "ProjectVar _" whenherbelin
2009-07-08Add heuristic based on non-linearity of evars to determine whether anherbelin
2009-07-08Fixing bug 2129 (evar introduced to remember an ambiguous projectionherbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-22documented a bug of pattern unification with metasbarras
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2009-04-03Fix obvious bug in evars_of_named_context.msozeau
2009-03-20Fixes to make Ynot compile with the trunk:msozeau
2009-03-04Backtrack sur la mémoïsation de nf_evar.aspiwack
2009-02-27=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...aspiwack
2009-02-20On passe les last_mods (un des champs de Evd.evar_defs) de listaspiwack
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-09memoized is_ground_envbarras
2009-02-06pushed evar reduction in kernelbarras
2009-02-06From v8.2 to trunk:herbelin
2009-01-20- Fixing bug 1891 (abusive instantiations of evar arguments inherbelin
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-17DISCLAIMERpuech
2009-01-05Completed 11745 (move of jprover to user contribs) and cleaned 11743herbelin
2009-01-04Fixed bugs #2001 (search_guard was overwriting the guard index givenherbelin
2008-11-21fixed problem with r11612barras
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
2008-11-07Fix universe problem appearing ConCaT using the existing infrastructure formsozeau
2008-11-05Fix in the unification algorithm using evars: unify types of evarmsozeau
2008-09-25Partial fix for bug #1948: recompute order of dependencies betweenmsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-29Correction d'un bug dans l'analyse des contraintes non résoluesherbelin
2008-06-21Various improvements in handling of evars in general and typingmsozeau
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
2008-05-20Correction d'un bug de l'unification pattern qui oubliait d'expanserherbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-04-18Correction bug 1835 + correction bug occur-check résultant en unherbelin
2008-03-30Modifications diverses et variées :herbelin
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:53:15 +0000