diff options
Diffstat (limited to 'theories/setoid_ring/Ring_tac.v')
| -rw-r--r-- | theories/setoid_ring/Ring_tac.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/setoid_ring/Ring_tac.v b/theories/setoid_ring/Ring_tac.v index 76e9b1e947..9323ae23b9 100644 --- a/theories/setoid_ring/Ring_tac.v +++ b/theories/setoid_ring/Ring_tac.v @@ -41,7 +41,7 @@ Ltac Get_goal := match goal with [|- ?G] => G end. Ltac OnEquation req := match goal with | |- req ?lhs ?rhs => (fun f => f lhs rhs) - | _ => (fun _ => fail "Goal is not an equation (of expected equality)") + | _ => (fun _ => fail "Goal is not an equation (of expected equality)" req) end. Ltac OnEquationHyp req h := |