diff options
| author |  mlasson <marc.lasson@gmail.com> | 2015-06-25 19:50:15 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 00:47:37 +0200 |
| commit | 60b5e9c05e0c168e30eafede545c221e63d12ea2 (patch) | |
| tree | 3691a6b1a108157eaf6a8eb79f192f1f23d8675a | |
| parent | 518049fe7f689489842fdfa670f57b618f125f31 (diff) | |
Also there's an extra space in the error message.
| -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 ac8ca3a11..7a3bcfba8 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1086,7 +1086,7 @@ let error_bad_ind_parameters env c n v1 v2 = let pv1 = pr_lconstr_env env Evd.empty v1 in let pv2 = pr_lconstr_env env Evd.empty v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ - str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "." + str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = str "The name" ++ spc () ++ pr_id id ++ spc () ++ |