aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Scheme.v
blob: dd5aa81d1d6e48c429d629dbb16b2310813871bb (plain)
1
2
3
4
(* This failed in 8.3pl2 *)

Scheme Induction for eq Sort Prop.
Check eq_ind_dep.