aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-13 00:47:47 +0200
committerHugo Herbelin2020-12-09 11:04:47 +0100
commit3f286f3fcb846cac360969372d71e91c5aefe810 (patch)
treeab4ff9b39ab12c43332bb290c8f6e971f6391a70 /interp
parenta386c2f1ba38ea106a1da386eddd029bd9b66e37 (diff)
Adding functions to returning the def/decl status of an inductive arity.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions