aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-09 18:57:10 +0100
committerEmilio Jesus Gallego Arias2018-11-09 18:57:10 +0100
commit7e3c54c09bdd748e2e2a60a94891b65481776041 (patch)
tree8635c000d2d5f67b12b9058a3fc6d6c9579d1db3 /kernel/inductive.ml
parent1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (diff)
parentc5213ab2a33087286a7ef224b8d2c73f8d19176d (diff)
Merge PR #8956: Fix dune runtest invocation
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions