diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-22 10:09:39 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-22 10:09:39 +0200 |
| commit | 5b13c78e65a282bde23517f2da4059beb551dd9e (patch) | |
| tree | 399f644272425be0b68360d63ae1ebe9de13972e /cparser/Elab.ml | |
| parent | 7aa563e8d3730e37f42979989f2fa87c940a4d4b (diff) | |
| download | compcert-5b13c78e65a282bde23517f2da4059beb551dd9e.tar.gz compcert-5b13c78e65a282bde23517f2da4059beb551dd9e.zip | |
Nicer error message for redefinitions with incompatible type
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1888f053..76f8efdb 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -115,11 +115,12 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Some new_ty -> new_ty | None -> + let id = Env.fresh_ident s in error loc "redefinition of '%s' with incompatible type.@ \ - Previous type: %a.@ \ - New type: %a" - s Cprint.typ old_ty Cprint.typ ty; + Previous declaration: %a.@ \ + New declaration: %a" + s Cprint.simple_decl (id, old_ty) Cprint.simple_decl (id, ty); ty in let new_sto = (* The only case not allowed is removing static *) |