diff options
author | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /toplevel/himsg.ml | |
parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r-- | toplevel/himsg.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f550df16..2ef8bd2b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -851,8 +851,8 @@ let error_same_names_overlap idl = str "names:" ++ spc () ++ prlist_with_sep pr_comma pr_id idl ++ str "." -let error_not_an_arity id = - str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity." +let error_not_an_arity env c = + str "The type" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "is not an arity." let error_bad_entry () = str "Bad inductive definition." @@ -888,7 +888,7 @@ let explain_inductive_error = function | SameNamesTypes id -> error_same_names_types id | SameNamesConstructors id -> error_same_names_constructors id | SameNamesOverlap idl -> error_same_names_overlap idl - | NotAnArity id -> error_not_an_arity id + | NotAnArity (env, c) -> error_not_an_arity env c | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () |