aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-10-19 14:14:42 +0200
committerMatthieu Sozeau2016-10-20 10:09:06 +0200
commitb7f8221739ea0822b67e463774e108f8813ffaf3 (patch)
treec98984d3105a3a18b81bac1fa0e4a36a8a5954e6 /dev/doc
parent00978cddf6e2da71892de6362e69c372429e159f (diff)
Refine printing of pending unification constraints
It now prints evars with candidates as well if there are any.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions