diff options
| author | herbelin | 2011-08-10 19:20:49 +0000 |
|---|---|---|
| committer | herbelin | 2011-08-10 19:20:49 +0000 |
| commit | f1e41151480f94ebf72e1c1af873365f5ec4a2e9 (patch) | |
| tree | 4cba365900532cf497c0704857e820818eb48f49 | |
| parent | c468066951baafc1164261f58c61dd601619bcc8 (diff) | |
Improving error message about coinductive guard (old "cases" is now "match")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14405 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/himsg.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ff578270a8..06fc7e663a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -289,12 +289,12 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = str "Recursive call forbidden in the type of a recursive definition" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseFun c -> - str "Recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c + str "Invalid recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseArg c -> - str "Recursive call in the argument of cases in" ++ spc () ++ + str "Invalid recursive call in the argument of \"match\" in" ++ spc () ++ pr_lconstr_env env c | RecCallInCasePred c -> - str "Recursive call in the type of cases in" ++ spc () ++ + str "Invalid recursive call in the \"return\" clause of \"match\" in" ++ spc () ++ pr_lconstr_env env c | NotGuardedForm c -> str "Sub-expression " ++ pr_lconstr_env env c ++ |