aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r--kernel/inductive.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3b64a2c09c..8ff8ddb85e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -218,7 +218,7 @@ let type_of_constructor cstr (mib,mip) =
let specif = mip.mind_user_lc in
let i = index_of_constructor cstr in
let nconstr = Array.length mip.mind_consnames in
- if i > nconstr then error "Not enough constructors in the type";
+ if i > nconstr then error "Not enough constructors in the type.";
constructor_instantiate (fst ind) mib specif.(i-1)
let arities_of_specif kn (mib,mip) =