From 3fec5b50cd2ff6fd70b4b3bae2fafa53d5e55261 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 4 Feb 2004 22:13:23 +0000 Subject: Boite autour des quote pour eviter un retour a la ligne apres le premier guillement; quote seulement en v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5291 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/himsg.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c74914e42..2b7688f8d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -28,11 +28,11 @@ open Printer open Ast open Rawterm -let quote s = str "\"" ++ s ++ str "\"" +let quote s = if !Options.v7 then s else h 0 (str "\"" ++ s ++ str "\"") let prterm c = quote (prterm c) let prterm_env e c = quote (prterm_env e c) -let prjudge_env e c = let v,t = prjudge_env e c in (quote v, quote t) +let prjudge_env e c = let v,t = prjudge_env e c in (quote v,quote t) let nth i = let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in @@ -117,7 +117,7 @@ let explain_case_not_inductive ctx cj = | Evar _ -> str "Cannot infer a type for this expression" | _ -> - str "This term" ++ brk(1,1) ++ pc ++ spc () ++ + str "The term" ++ brk(1,1) ++ pc ++ spc () ++ str "has type" ++ brk(1,1) ++ pct ++ spc () ++ str "which is not a (co-)inductive type" -- cgit v1.2.3