ImportedCoercion.v « failure « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/failure/ImportedCoercion.v

blob: 0a69b85172c1aff9296f16348beee7b80a243073 (plain)

(* Test visibility of coercions *)

Require Import make_local.

(* Local coercion must not be used *)

Check (0 = true).