index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarsolve.mli
Commit message (
Expand
)
Author
Age
*
Renamings to avoid confusion deprecating old names
Matthieu Sozeau
2016-10-22
*
congruence: Restrict refreshing to Set
Matthieu Sozeau
2016-07-04
*
congruence/univs: properly refresh (fix #4609)
Matthieu Sozeau
2016-07-04
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fix bug #4293: ensure let-ins do not contain algebraic universes in
Matthieu Sozeau
2015-11-11
*
Update headers.
Maxime Dénès
2015-01-12
*
Work around issues with FO unification trying to unify terms of
Matthieu Sozeau
2014-10-02
*
Move the specific map_constr_with_binders_left_to_right
Matthieu Sozeau
2014-09-19
*
Fix constrMatching as well as change/e_contextually to allow
Matthieu Sozeau
2014-09-18
*
Make evarconv and unification able to handle eta for records in presence
Matthieu Sozeau
2014-08-26
*
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
Matthieu Sozeau
2014-08-25
*
Avoid introducing additional universes when doing pruning in evarsolve.
Matthieu Sozeau
2014-07-30
*
Change interface of refresh universes to get a pbty argument instead of
Matthieu Sozeau
2014-06-26
*
- Add an option to refresh only algebraic universes, for e_type_of. The goal
Matthieu Sozeau
2014-06-21
*
Cleanup treatment of template universe polymorphism (thanks to E. Tassi
Matthieu Sozeau
2014-06-20
*
Find a more efficient fix for dealing with template universes:
Matthieu Sozeau
2014-05-06
*
Try a new way of handling template universe levels
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Propagating conversion_problem towards (postponed) evar/evar problems.
Hugo Herbelin
2014-04-01
*
Removing useless array-to-list and converse casts used in
ppedrot
2013-10-22
*
Continuation of r16346 on filtering local definitions. Refined
herbelin
2013-03-30
*
Repairing r16205: errors raised by check_evar_instance were no longer
herbelin
2013-02-28
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Splitted Evarutil in two files
ppedrot
2013-02-10