aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Expand)AuthorAge
* 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
* (Try to) use the conversion oracle also in w_unify to choose which constant toGravatar msozeau2008-10-03
* Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anGravatar msozeau2008-09-04
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)Gravatar herbelin2008-06-21
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)Gravatar barras2008-06-05
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* refined the conversion oracleGravatar barras2008-05-21
* Correction d'un bug de l'unification pattern qui oubliait d'expanserGravatar herbelin2008-05-20
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-30 02:30:19 +0000