aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/bug_3312.v
blob: bf87c3995f8ee4aee1c4437c86775e97366395f1 (plain)
1
2
3
4
5
6
Require Import Setoid.
Axiom bar : 0 = 1.
Goal 0 = 1.
  Fail rewrite_strat bar. (* Toplevel input, characters 15-32:
Error: Tactic failure:setoid rewrite failed: Nothing to rewrite. *)
Abort.