test-suite/bugs/closed/2350.v


1
2
3
4
5
6

(* 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) := _).