summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_4836.v
blob: 5838dcd8a773e16dbdf7f4795b624e405b5e0983 (plain)
1
(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)