From 5b13c78e65a282bde23517f2da4059beb551dd9e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 22 Jul 2016 10:09:39 +0200
Subject: Nicer error message for redefinitions with incompatible type

---
 cparser/Elab.ml | 7 ++++---
 1 file 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 *)
-- 
cgit