aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/indtypes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 12f1760407..4ab8d3cb53 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -204,7 +204,7 @@ let type_inductive env mie =
if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
(* Check unicity of names *)
mind_check_names mie;
- mind_check_arities env mie
+ mind_check_arities env mie;
(* We first type params and arity of each inductive definition *)
(* This allows to build the environment of arities and to share *)
(* the set of constraints *)