aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.mli
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Make evarconv and unification able to handle eta for records in presenceGravatar Matthieu Sozeau2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Avoid introducing additional universes when doing pruning in evarsolve.Gravatar Matthieu Sozeau2014-07-30
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* - Add an option to refresh only algebraic universes, for e_type_of. The goalGravatar Matthieu Sozeau2014-06-21
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Propagating conversion_problem towards (postponed) evar/evar problems.Gravatar Hugo Herbelin2014-04-01
* Removing useless array-to-list and converse casts used inGravatar ppedrot2013-10-22
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
* Repairing r16205: errors raised by check_evar_instance were no longerGravatar herbelin2013-02-28
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10