diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml new file mode 100644 index 0000000000..82da97329a --- /dev/null +++ b/kernel/indtypes.ml @@ -0,0 +1,13 @@ + +(* $Id$ *) + +open Inductive +open Environ +open Reduction + +let mind_check_arities env mie = + let check_arity id c = + if not (is_arity env c) then raise (InductiveError (NotAnArity id)) + in + List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds + |