diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-30 12:09:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-30 12:11:43 +0200 |
| commit | f0a85b61cce59e55675df0ba6c9297166d757ce0 (patch) | |
| tree | 9ba9711120c2035f5534880a579ed6a5d1abf12f /vernac/himsg.ml | |
| parent | 7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (diff) | |
Fixing a capitalization in the middle of the sentence of an error message.
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 "." |