summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/3312.v
blob: 749921e2f66445f37f0d6e7d1763e03fa7edcd72 (plain)
1
2
3
4
5
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. *)