aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-03-04 00:52:24 +0100
committerGaëtan Gilbert2018-04-13 14:10:04 +0200
commitc097b83dc9a33a2410e61b8d2aa667229fbd411c (patch)
tree99d59f20fc255d39ce1827486f79a457e6ce5e4e /pretyping/typeclasses_errors.ml
parent0099a8f8e1a77a224ff133fc211d5a8b983a7dcc (diff)
univ minimization: let-lift [not_lower]
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions