aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
AgeCommit message (Expand)Author
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-04-05Granting wish #2251 (forbidding rewriting a term reduced to an evar)herbelin
2010-04-05Partial fix to bug #2244 (ensure that pattern unification does notherbelin
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
2010-02-22Improve unification when evars and metas are mixed.msozeau
2010-01-26Quick fix for references to section variables unbound in the currentmsozeau
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-04Changed the way to support compatibility with previous versions.herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-11Relatively ad hoc fix to an ill-typed instantiation bug in typeherbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-07-15- Fixing bug #2139 (kernel-based test of well-formation of eliminationherbelin
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-30Add new variants of [rewrite] and [autorewrite] which differ in themsozeau
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
2009-06-02Backtrack on experimental unification with sort variables: it requires msozeau
2009-06-01Change unification with sort constraints to not use the kernelmsozeau
2009-05-28Properly catch sort constraint inconsistency exception inmsozeau
2009-05-27Populate the sort constraints set correctly during unification. Add amsozeau
2009-05-24Temporary fixes in unification:msozeau
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
2009-05-20Many fixes in unification:msozeau
2009-05-19Fix in canonical structure resolution: [check_conv_record] may returnmsozeau
2009-05-18Minor unification changes:msozeau
2009-05-16(Tentative to) add Canonical Structure resolution to the regularmsozeau
2009-04-09Backtrack on 12061 (type checking for bug #2084 too strong as soon as we useherbelin
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
2009-01-20Fixing bug #1918 (no occur-check in Meta unification was done yet!).herbelin
2009-01-12Fix a bunch of bugs related to setoid_rewrite, unification and evars:msozeau
2009-01-04Fixed bugs #2001 (search_guard was overwriting the guard index givenherbelin
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-12-04Fixes for unification and substitution of metas under binders.msozeau
2008-12-02Miscellaneous fixes and improvements:herbelin
2008-11-14Restores behaviour of v8.1 for unification problems which fail (backport of 1...letouzey
2008-11-05Fix in the unification algorithm using evars: unify types of evarmsozeau
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-10-09* Fixed constr_cmp again to handle universes subtyping correctlypuech
2008-10-03(Try to) use the conversion oracle also in w_unify to choose which constant tomsozeau
2008-09-04Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anmsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-06-21Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)herbelin
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 12:59:37 +0000