aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/bug_3311.v
blob: 23752acf1c8a2eb45740ca8c115fe4c5f4877aeb (plain)
1
2
3
4
5
6
7
8
9
10
11
Require Import Setoid.
Axiom bar : True = False.
Goal True.
  Fail setoid_rewrite bar. (* Toplevel input, characters 15-33:
Error:
Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints.

Could not find an instance for "subrelation eq (Basics.flip Basics.impl)".
With the following constraints:
?3 : "True" *)
Abort.