5750.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: 6d0e21f5d007ebb37a7ae5a2202742004b616050 (plain)

1
2
3

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