test-suite/bugs/closed/3798.v


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.