aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorHugo Herbelin2017-11-06 21:09:00 +0100
committerHugo Herbelin2017-12-23 02:35:58 +0100
commitb455e96cce263ea48ff0aa8b8ebf530d0f1eea9c (patch)
treecb2123b0eebe67878b219fab6efbd7a5314e9610 /pretyping/typeclasses.mli
parent19a584d3fa9594abdf3dcc0148f368547ce77ccc (diff)
Registering a printing handler in coq_makefile.
This allows to fix the non-printing of error messages produced when parsing arguments.
Diffstat (limited to 'pretyping/typeclasses.mli')
0 files changed, 0 insertions, 0 deletions