1 2 3 4 5 6 7
(* Test visibility of coercions *) Require Import make_local. (* Local coercion must not be used *) Check (0 = true).