From ea26a4f7937bedbae4cf81d021283b9f72eec074 Mon Sep 17 00:00:00 2001
From: gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 5 Apr 2012 10:53:42 +0000
Subject: Relax uniform inheritance condition

Uniform inheritance is not always needed for the coercion mechanism
to work. We turn it into a warning.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15117 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/class.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 79d7a99fd..be2482a2b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -256,7 +256,7 @@ let add_new_coercion_core coef stre source target isid =
   in
   check_source (Some cls);
   if not (uniform_cond (llp-ind) lvs) then
-    raise (CoercionError NotUniform);
+    warning (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform));
   let clt =
     try
       get_target tg ind
-- 
cgit v1.2.3