aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3798.v
blob: b9f0daa71c227c6854ec3bbcb37a87b948284f3f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Require Import TestSuite.admit.
Require Setoid.

Parameter f : nat -> nat.
Axiom a : forall n, 0 < n -> f n = 0.
Hint Rewrite a using ( simpl; admit ).

Goal f 1 = 0.
Proof.
  rewrite_strat (topdown (hints core)).
  reflexivity.
Qed.