aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-11-17 11:28:42 +0100
committerPierre-Marie Pédrot2014-11-17 12:07:18 +0100
commit46c93445392543affd40412460d8ca436f5cfb84 (patch)
treebd71f99b5791953c33482d521b56fad33a02ab8f /kernel/nativevalues.ml
parent35b88621408d13ae8e2a0247daa01d95d749161c (diff)
Setting printing tags for Ltac.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions