aboutsummaryrefslogtreecommitdiff
path: root/API/grammar_API.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-19 17:43:19 +0200
committerMaxime Dénès2017-06-19 17:43:19 +0200
commit414890675cb72fd9286e19521a746677c06e784e (patch)
tree14599a23215356ac472ac483ad564c11eb53c1fc /API/grammar_API.ml
parent396c77feb0cced3965f90f65c681e48c528636d5 (diff)
parent15b1856edd593b39d63d23584a4f5acec0eeb592 (diff)
Merge PR#613: Cumulativity for inductive types
Diffstat (limited to 'API/grammar_API.ml')
0 files changed, 0 insertions, 0 deletions