aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-12-16 13:54:40 +0100
committerPierre-Marie Pédrot2018-12-16 13:54:40 +0100
commit7e155688331c8f004f34950da67108d7284e4e56 (patch)
tree9182191cd348bc32eaa8cdd00b615a924ed17c6f /interp/notation.ml
parent2a7992f75c86a15512568ac61ca4c43e23242b28 (diff)
parenta2549c7f716e870ea19fdbfd7b5493117fe21e76 (diff)
Merge PR #9172: [proof] Rework proof interface.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions