From cbcf2f8950d0ea7208d9c021422946433f90e745 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 8 Jul 2015 10:49:36 +0200
Subject: Turn "redefinition with an incompatible type" warning into an error.

Also: improve error message by showing old and new types.
---
 cparser/Elab.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'cparser')

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index d6b79780..5be4c598 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1805,7 +1805,12 @@ let enter_or_refine_ident local loc env s sto ty =
         | Some new_ty ->
             new_ty
         | None ->
-            warning loc "redefinition of '%s' with incompatible type" s; ty in
+            error loc
+               "redefinition of '%s' with incompatible type.@ \
+                Previous type: %a.@ \
+                New type: %a"
+              s Cprint.typ old_ty Cprint.typ ty;
+            ty in
       let new_sto =
 	(* The only case not allowed is removing static *)
 	match old_sto,sto with
-- 
cgit