aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Restored a "feature" of unification in pre-8.3 (it was used e.g. in aGravatar herbelin2010-06-25
* Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).Gravatar herbelin2010-06-18
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").Gravatar herbelin2010-04-11
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Granting wish #2251 (forbidding rewriting a term reduced to an evar)Gravatar herbelin2010-04-05
* Partial fix to bug #2244 (ensure that pattern unification does notGravatar herbelin2010-04-05
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
* Improve unification when evars and metas are mixed.Gravatar msozeau2010-02-22
* Quick fix for references to section variables unbound in the currentGravatar msozeau2010-01-26
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
* Change unification with sort constraints to not use the kernelGravatar msozeau2009-06-01
* Properly catch sort constraint inconsistency exception inGravatar msozeau2009-05-28
* Populate the sort constraints set correctly during unification. Add aGravatar msozeau2009-05-27
* Temporary fixes in unification:Gravatar msozeau2009-05-24
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* Many fixes in unification:Gravatar msozeau2009-05-20
* Fix in canonical structure resolution: [check_conv_record] may returnGravatar msozeau2009-05-19
* Minor unification changes:Gravatar msozeau2009-05-18
* (Tentative to) add Canonical Structure resolution to the regularGravatar msozeau2009-05-16
* Backtrack on 12061 (type checking for bug #2084 too strong as soon as we useGravatar herbelin2009-04-09
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Fixing bug #1918 (no occur-check in Meta unification was done yet!).Gravatar herbelin2009-01-20
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Fixes for unification and substitution of metas under binders.Gravatar msozeau2008-12-04
* Miscellaneous fixes and improvements:Gravatar herbelin2008-12-02
* Restores behaviour of v8.1 for unification problems which fail (backport of 1...Gravatar letouzey2008-11-14
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* * Fixed constr_cmp again to handle universes subtyping correctlyGravatar puech2008-10-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 19:23:06 +0000