aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-25 13:29:43 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-26 10:55:32 +0200
commit5474d83bc8845bd5aa3fb339057d6efa5feedd7a (patch)
treee83a81ab2bd17e7319b6f1b1dd301839cbed041b /kernel/names.mli
parentb5216429572b4737ca2b2600788e8e3246f1d685 (diff)
COMMENT: Proofview.entry
Diffstat (limited to 'kernel/names.mli')
0 files changed, 0 insertions, 0 deletions