diff options
| author | Pierre-Marie Pédrot | 2020-11-20 15:17:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-20 15:17:31 +0100 |
| commit | dac6017513cea37f96ce8256239e490f18339f08 (patch) | |
| tree | eae43761e97bdd403553182eec7afce51c3fa7a8 /theories | |
| parent | 04186f83545e3c693976c73d488b36dd4a2b50db (diff) | |
| parent | f2a5096bf0829316eba869fe5d929337e6fd8bad (diff) | |
Merge PR #13399: Miscellaneous ring improvements in code + error messages
Reviewed-by: ppedrot
Diffstat (limited to 'theories')
| -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 := |