aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorEnrico Tassi2016-06-16 13:33:52 +0200
committerEnrico Tassi2016-06-16 13:33:52 +0200
commit3d308cc39c4e545155d5ad27b49a65cf10f27567 (patch)
treeae8f2a5f93d2ccdf743489ce6e26f94efa9d7939 /kernel/inductive.ml
parent7f416bad62c0a94a0ff2fbdb433d03f3d5366ad6 (diff)
Ignore generated .ml file for ssrmatching
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions