path: root/test-suite/bugs/closed/bug_4217.v

(* Checking correct index of implicit by pos in fixpoints *)

Fixpoint ith_default
         {default_A : nat}
         {As : list nat}
         {struct As} : Set.
Abort.