aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3616.v
blob: 688700260c2f537dc56f407580ac227057ea2b95 (plain)
1
2
3
(* Was failing from April 2014 to September 2014 because of injection *)
Goal forall P e es t, (e :: es = existT P tt t :: es)%list -> True.
inversion 1.