summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3623.v
blob: 202b900164427a0c3751aaf7457b259914b4b1b2 (plain)
1
2
3
4
Require Import List.
Goal  (1 :: 2 :: nil) ++ (3::nil) = (1::2::3::nil).
change (@app nat (?a :: ?b) ?c) with (a :: @app nat b c).
Abort.