aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Expand)AuthorAge
* - Remove create_evar_defsGravatar msozeau2011-04-13
* - Improve unification (beta-reduction, and same heuristic as evarconv for red...Gravatar msozeau2011-04-13
* Unify meta types with the right flags, add betaiotazeta reduction to unificat...Gravatar msozeau2011-04-13
* Proper typing of metavariables, type errors were completely ignored before......Gravatar msozeau2011-04-13
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Solve evar instantiations in the right environment.Gravatar msozeau2011-03-08
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 02:09:44 +0000