diff options
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 2be10a039..e15911dd6 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1176,7 +1176,7 @@ let error_not_allowed_case_analysis isrec kind i = pr_inductive (Global.env()) (fst i) ++ str "." let error_not_allowed_dependent_analysis isrec i = - str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ + str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++ strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) i ++ str "." |