summaryrefslogtreecommitdiff
path: root/test-suite/output/Match_subterm.v
blob: 2c44b1879ffafd15a180a51b66301fce534ef6e5 (plain)
1
2
3
4
5
6
Goal 0 = 1.
match goal with
| |- context [?v] =>
  idtac v ; fail
| _ => idtac 2
end.