diff options
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 32de48cd7b..01e83b1ad0 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -672,7 +672,7 @@ let error_not_allowed_case_analysis isrec kind i = let error_not_mutual_in_scheme ind ind' = if ind = ind' then str "The inductive type " ++ pr_inductive (Global.env()) ind ++ - str "occurs twice." + str " occurs twice." else str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++ str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++ |