diff options
| author | ppedrot | 2013-08-04 19:15:28 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-04 19:15:28 +0000 |
| commit | 4372b5bc27e7ffcb4bff2cf5c093cdbafeddfe83 (patch) | |
| tree | 0b76ad21b4123268a6338610bad4b2b468c3aac1 /toplevel | |
| parent | 6fb58f97c756fcd4841876edc6da4001d23d8bbb (diff) | |
Fixing #2846: Uncaught exception Reduction.NotArity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16662 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -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 616dfb9417..6f7696fabe 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -908,8 +908,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." @@ -945,7 +945,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 () |