From c3c747475f5818445438e779bed0685e01306eff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 10 Jun 2014 19:36:37 +0200
Subject: Removing explanations of universe inconsistencies from the checker.
 They were never used and were responsible for code duplication.

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

(limited to 'checker/checker.ml')

diff --git a/checker/checker.ml b/checker/checker.ml
index f3c583b83..b39fc2af7 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -251,7 +251,7 @@ let rec explain_exn = function
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
   | Sys.Break ->
       hov 0 (fnl () ++ str "User interrupt.")
-  | Univ.UniverseInconsistency (o,u,v,_) ->
+  | Univ.UniverseInconsistency (o,u,v) ->
       let msg =
 	if !Flags.debug (*!Constrextern.print_universes*) then
 	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
-- 
cgit v1.2.3