diff options
| author | Vincent Semeria | 2020-05-31 09:38:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 20:30:08 +0100 |
| commit | f2a5096bf0829316eba869fe5d929337e6fd8bad (patch) | |
| tree | 5a512b72750bf5121f73886103060f6bdee7c28b /theories/setoid_ring | |
| parent | 68bd3b4e3f9932ef4b3f2afd260cec8780ae155f (diff) | |
Improve some error messages.
This also includes aligning with refman when relevant and using capital
letters and final period.
Diffstat (limited to 'theories/setoid_ring')
| -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 := |