aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.mli
Commit message (Expand)AuthorAge
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Dedicated datatype for aliases in Evarsolve.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
|/
* congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
* congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 13:43:58 +0000