aboutsummaryrefslogtreecommitdiff
path: root/kernel/opaqueproof.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-05-15 23:50:42 +0200
committerPierre-Marie Pédrot2019-05-19 13:14:19 +0200
commit801aed67a90ec49c15a4469e1905aa2835fabe19 (patch)
tree9da139e5e0e5ecd8ba74806d2baa1225cee2e720 /kernel/opaqueproof.ml
parent925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d (diff)
Parameterize the constant_body type by opaque subproofs.
Diffstat (limited to 'kernel/opaqueproof.ml')
0 files changed, 0 insertions, 0 deletions