aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-07-07 14:25:20 +0200
committerGaëtan Gilbert2020-11-16 11:12:44 +0100
commit9990bea3e163850c0ac4dca982c73d2b2bc19a38 (patch)
tree28d9ddc1dec90446dbbbcfb448dcce80862431a8 /interp/constrexpr.ml
parent779d2b915a970cdfc87d3d1b69e10bab04094f33 (diff)
Infrastructure for cumulative inductive syntax (no grammar extension yet)
Diffstat (limited to 'interp/constrexpr.ml')
0 files changed, 0 insertions, 0 deletions