aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrexpr_ops.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-12-05 12:53:08 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-23 22:13:57 +0100
commit01622922a3a68cc4a0597bb08e0f7ba5966a7144 (patch)
tree2f49cfa0cf3239a25d6fef91149e320e6f0e4037 /interp/constrexpr_ops.mli
parentd2830ca4adf062df96d5e8978d4254cf5ece30c4 (diff)
Documenting the grammar {| ... |} syntax for building records.
And an extra minor changes (use of zeroone when relevant, use of type rather than term).
Diffstat (limited to 'interp/constrexpr_ops.mli')
0 files changed, 0 insertions, 0 deletions