aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorAmin Timany2017-05-23 23:28:39 +0200
committerEmilio Jesus Gallego Arias2017-06-16 04:51:18 +0200
commite28d3a488c81c6dc59aa8f53d98a95ee93a84d37 (patch)
tree857104e88a1619008ef1e6a15ec476b5a58b7573 /kernel/nativecode.ml
parent7b323421ba558011c304a686c4cd368e1ff39440 (diff)
Document cumulativity for inductive types
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions