aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-04 15:22:07 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-04 15:22:07 +0200
commitf3b714f5a8e516ee9731d705808a4084caae5a1e (patch)
tree5811499a4d0d97f4b6b5de73beab3b32a6ce456e /pretyping/pretyping.mli
parentc9d9e0ffa4bd3efb9366726f3c78374d71f87b8b (diff)
More explicit printing in Himsg.
Diffstat (limited to 'pretyping/pretyping.mli')
0 files changed, 0 insertions, 0 deletions