ImportedCoercion.v « failure « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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

blob: 1cac69f4b369630b5e1ee8d7074e70e2e20cc1c9 (plain)

(* Test visibility of coercions *)

Require Import make_local.

(* Local coercion must not be used *)

Fail Check (0 = true).