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

(* Check that the fix tactic, when called from refine, reduces enough
   to see the products *)

Definition foo := forall n:nat, n=n.
Definition bar : foo.
refine (fix aux (n:nat) := _).
Abort.