diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-04 22:13:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-04 22:13:23 +0000 |
| commit | 3fec5b50cd2ff6fd70b4b3bae2fafa53d5e55261 (patch) | |
| tree | 2f72d95a08ca4d6429355477f1f03f50ad73d4ba | |
| parent | 324f9d73cb3ce3da4248ca720ebd80ab77f7de84 (diff) | |
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
| -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 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" |