diff options
| author | herbelin | 2004-03-17 00:05:57 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-17 00:05:57 +0000 |
| commit | e964da1ad108e2bc1f5f01f4ad041c10a07f5d6f (patch) | |
| tree | e5cb9540dc95b32ef3cb2348121bdb85e9d77801 | |
| parent | 0cbcf76dc9ffa1f71c6aa5a8f255c9a3225163cc (diff) | |
Message d'erreur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5511 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |