aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xpretyping/classops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4cd71d09d1..76925e23e7 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -309,7 +309,7 @@ let add_coercion_in_graph (ic,source,target) =
end)
old_inheritance_graph
end;
- if (!ambig_paths <> []) & is_mes_ambig() then
+ if (!ambig_paths <> []) && is_verbose () && is_mes_ambig() then
pPNL (message_ambig !ambig_paths)
let cache_coercion (_,((coe,xf),cls,clt)) =