Hopefully improved layout of fix guardness error message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12445 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 9 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 99e228dd46..6b8c45fec2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -233,21 +233,20 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
         match names.(j) with
             Name id -> pr_id id
           | Anonymous -> str "the " ++ nth i ++ str " definition" in
+      let pr_db x = quote (pr_db env x) in
       let vars =
         match (lt,le) with
             ([],[]) -> assert false
-          | ([],[x]) ->
-              str "a subterm of " ++ pr_db env x
-          | ([],_) ->
-              str "a subterm of the following variables: " ++
-              prlist_with_sep pr_spc (pr_db env) le
-          | ([x],_) -> pr_db env x
+          | ([],[x]) -> str "a subterm of " ++ pr_db x
+          | ([],_) -> str "a subterm of the following variables: " ++
+              prlist_with_sep pr_spc pr_db le
+          | ([x],_) -> pr_db x
           | _ ->
               str "one of the following variables: " ++
-              prlist_with_sep pr_spc (pr_db env) lt in
+              prlist_with_sep pr_spc pr_db lt in
       str "Recursive call to " ++ called ++ spc () ++
-      str "has principal argument equal to" ++ spc () ++
-      pr_lconstr_env env arg ++ fnl () ++ str "instead of " ++ vars
+      strbrk "has principal argument equal to" ++ spc () ++
+      pr_lconstr_env env arg ++ strbrk " instead of " ++ vars
 
   | NotEnoughArgumentsForFixCall j ->
       let called =