aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.ml
diff options
context:
space:
mode:
authorHugo Herbelin2018-04-19 10:30:08 +0200
committerHugo Herbelin2018-05-02 19:25:22 +0200
commit880fee8f80503fc8a40e2e07b565cfd2a99d24da (patch)
tree67222b783e941aa265a425e1d9162a8c81d8538c /pretyping/typeclasses_errors.ml
parentfd146ca38202c9843b4240cbdac0ae75f57e4d67 (diff)
Make "intro"/"intros" progress on existential variables.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions