aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-01-17 19:06:10 +0530
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-01-18 00:16:44 +0530
commit1c0110b40a9009aa6b56fafbf34a04e7ae59de0f (patch)
tree1729539171e7f098b0b724b65da6cc1ce9f3b37f /pretyping/detyping.mli
parentd187edf437ca4dac73b1da5d434cdf164c129319 (diff)
Univs: Complete documentation in refman.
Diffstat (limited to 'pretyping/detyping.mli')
0 files changed, 0 insertions, 0 deletions