diff options
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 20a0adfc18..8723ec3c65 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,8 +1,10 @@ (* $Id$ *) +(*i*) open Inductive open Environ +(*i*) (* [mind_check_arities] checks that the types declared for all the inductive types are some arities. *) |