aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-18 12:06:24 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-18 12:26:27 +0100
commiteee16239f6b00400c8a13b787c310bcb11c37afe (patch)
treeb1974b3f1b4a3d2ea8f8441d95789049326762d2 /kernel/names.mli
parentd83e8aceaca972f8997f208e46d257e69c2e352d (diff)
Tying the loop in tactic printing API.
Diffstat (limited to 'kernel/names.mli')
0 files changed, 0 insertions, 0 deletions