Déplacement surround dans util.ml et parenthésage des déclarations

castées si aussi suivies de leur type (p.ex. dans les hypothèses de but),
afin d'éviter des configurations non réinterprétables comme x:nat:nat.


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

6 files changed, 7 insertions, 4 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 599e17adf..dc25caefe 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -813,6 +813,8 @@ let prvect_with_sep sep elem v =
   let n = Array.length v in
   if n = 0 then mt () else pr (n - 1)
 
+let surround p = hov 1 (str"(" ++ p ++ str")")
+
 (*s Size of ocaml values. *)
 
 module Size = struct
diff --git a/lib/util.mli b/lib/util.mli
index a5089a2de..9951aa1c5 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -240,6 +240,8 @@ val prlist_with_sep :
 val prvect_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val surround : std_ppcmds -> std_ppcmds
+
 
 (*s Size of an ocaml value (in words, bytes and kilobytes). *)
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index ea4a26308..4ac2cbe9e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -95,8 +95,6 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let surround p = hov 1 (str"(" ++ p ++ str")")
-
 let pr_located pr ((b,e),x) =
   if Options.do_translate() && (b,e)<>dummy_loc then
     let (b,e) = unloc (b,e) in
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 254a789c0..f354ac44f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -261,8 +261,6 @@ let rec pr_tacarg_using_rule pr_gen = function
   | [], [] -> mt ()
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let surround p = hov 1 (str"(" ++ p ++ str")")
-
 let pr_extend_gen prgen lev s l =
   try 
     let tags = List.map genarg_tag l in
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index d05f4ffd4..fa839587f 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -246,6 +246,7 @@ let print_safe_judgment env j =
 let print_named_def name body typ =
   let pbody = pr_lconstr body in
   let ptyp = pr_ltype typ in
+  let pbody = if isCast body then surround pbody else pbody in
   (str "*** [" ++ str name ++ str " " ++
      hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
 	      str ":" ++ brk (1,2) ++ ptyp) ++
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 1b069c5ee..a128eb1a7 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -125,6 +125,7 @@ let pr_var_decl env (id,c,typ) =
     | Some c ->
 	(* Force evaluation *) 
 	let pb = pr_lconstr_env env c in
+	let pb = if isCast c then surround pb else pb in
 	(str" := " ++ pb ++ cut () ) in
   let pt = pr_ltype_env env typ in
   let ptyp = (str" : " ++ pt) in
@@ -136,6 +137,7 @@ let pr_rel_decl env (na,c,typ) =
     | Some c ->
 	(* Force evaluation *) 
 	let pb = pr_lconstr_env env c in
+	let pb = if isCast c then surround pb else pb in
 	(str":=" ++ spc () ++ pb ++ spc ()) in
   let ptyp = pr_ltype_env env typ in
   match na with