aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-05-11 10:30:49 +0200
committerPierre-Marie Pédrot2016-05-11 11:23:11 +0200
commit17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c (patch)
treebf8244fee91d6d0784a59c3dcdfe4e72507e1674 /kernel/inductive.ml
parentf2983cec3544473b18ebc4d4e3a20b941decd196 (diff)
Moving the grammar summary to Pcoq.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions