From 5f9a6c17b4353024e7510977a41cfb1de93a0f5f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 10 Jan 2019 14:43:56 +0100
Subject: Move inductive_error to Type_errors

---
 checker/checker.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index 167258f8bb..d97ab5409e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -297,7 +297,7 @@ let explain_exn = function
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
 
-  | Indtypes.InductiveError e ->
+  | InductiveError e ->
       hov 0 (str "Error related to inductive types")
 (*      let ctx = Check.get_env() in
       hov 0
-- 
cgit v1.2.3