bug_5750.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_5750.v

blob: d5527d9303a9fd604a8d0d82a48442e224cc24b8 (plain)

(* Check printability of the hole of the context *)
Goal 0 = 0.
match goal with |- context c [0] => idtac c end.
Abort.