diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-04 14:42:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-04 14:42:05 +0000 |
| commit | d57177a5aa5596cace507bd73a39ac3cd0db5b20 (patch) | |
| tree | ebe087b91a880544ab4ea147b9c114b50320dcd8 /toplevel/himsg.ml | |
| parent | b540ac616b3184bbd7e4710d4d9293c662b72ccb (diff) | |
Amelioration message d'erreur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4794 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3270ef451..e8fd76e43 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -326,7 +326,7 @@ let explain_unsolvable_implicit env = function | BinderType (Name id) -> str "Cannot infer a type for " ++ Nameops.pr_id id | BinderType Anonymous -> - str "Cannot infer a type of this anonymous binder" + str "Cannot infer a type for this anonymous binder" | ImplicitArg (c,n) -> str "Cannot infer the " ++ pr_ord n ++ str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c |