aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2350.v
blob: e91f22e2673cb1b403f6ff70d371c75812c9b656 (plain)
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) := _).