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/checkInductive.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'checker/checkInductive.mli')

diff --git a/checker/checkInductive.mli b/checker/checkInductive.mli
index 17ca0d4583..ab54190967 100644
--- a/checker/checkInductive.mli
+++ b/checker/checkInductive.mli
@@ -8,10 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(*i*)
 open Names
 open Environ
-(*i*)
+
+exception InductiveMismatch of MutInd.t * string
+(** Some field of the inductive is different from what the kernel infers. *)
 
 (*s The following function does checks on inductive declarations. *)
 
-- 
cgit v1.2.3