aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2019-03-21 08:21:40 +0100
committerThéo Zimmermann2019-03-21 08:21:40 +0100
commitce97ef5375e1596cd7b2510cf576f2961329f523 (patch)
tree8e1d835ecf89d93a754197e4d54017c99f287301 /kernel/inductive.ml
parent5c0a7041cba6f2d2654ddc34a3c63a11f494d430 (diff)
parente7ddf978adbf441d34b8c17502caaa05ee8da04b (diff)
Merge PR #9789: [Manual] Improve documentation on Section, Variable, Context
Reviewed-by: Zimmi48 Ack-by: jfehrle
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions