diff options
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 4ecdfb66ac..fcf60e396e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -988,8 +988,8 @@ let try_rewrite tac gls = errorlabstrm "try_rewrite" (str "Not a primitive equality here") | e when catchable_exception e -> errorlabstrm "try_rewrite" - (str "Cannot find a well type generalisation of the goal that" ++ - str " makes progress the proof.") + (str "Cannot find a well-typed generalization of the goal that" ++ + str " makes the proof progress") let subst l2r eqn cls gls = match cls with |