aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.mli
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-01Propagating conversion_problem towards (postponed) evar/evar problems.Hugo Herbelin
2013-10-22Removing useless array-to-list and converse casts used inppedrot
2013-03-30Continuation of r16346 on filtering local definitions. Refinedherbelin
2013-02-28Repairing r16205: errors raised by check_evar_instance were no longerherbelin
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-10Splitted Evarutil in two filesppedrot