summaryrefslogtreecommitdiff
path: root/toplevel/class.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/class.ml')
-rw-r--r--toplevel/class.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index ebaa19b6..c328cc91 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -255,7 +255,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