From 0f3c1f242ec824a5772c47de61a6cddebe2ee8c8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 20 Nov 2018 14:42:05 +0100
Subject: checker: check inductive types by roundtrip through the kernel.

---
 checker/checker.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'checker/checker.ml')

diff --git a/checker/checker.ml b/checker/checker.ml
index da6a61de1c..167258f8bb 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -302,6 +302,10 @@ let explain_exn = function
 (*      let ctx = Check.get_env() in
       hov 0
         (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
+
+  | CheckInductive.InductiveMismatch (mind,field) ->
+    hov 0 (MutInd.print mind ++ str ": field " ++ str field ++ str " is incorrect.")
+
   | Assert_failure (s,b,e) ->
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 	       (if s = "" then mt ()
-- 
cgit v1.2.3