Fixing test-suite after last storm in Pp.

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

2 files changed, 20 insertions, 25 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 7bd41cc221..2e8cc4023a 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -56,9 +56,9 @@ let gallina_print_modtype = print_modtype
 
 let print_closed_sections = ref false
 
-let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) ++ fnl()
+let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l)
 
-let with_line_skip l = if l = [] then mt() else fnl() ++ pr_infos_list l
+let with_line_skip l = if l = [] then mt() else fnl() ++ fnl () ++ pr_infos_list l
 
 let blankline = mt() (* add a blank sentence in the list of infos *)
 
@@ -355,7 +355,7 @@ let print_located_qualid ref =
 
 let gallina_print_typed_value_in_env env (trm,typ) =
   (pr_lconstr_env env trm ++ fnl () ++
-     str "     : " ++ pr_ltype_env env typ ++ fnl ())
+     str "     : " ++ pr_ltype_env env typ)
 
 (* To be improved; the type should be used to provide the types in the
    abstractions. This should be done recursively inside pr_lconstr, so that
@@ -390,7 +390,7 @@ let gallina_print_inductive sp =
   let env = Global.env() in
   let mib = Environ.lookup_mind sp env in
   let mipv = mib.mind_packets in
-  pr_mutual_inductive_body env sp mib ++ fnl () ++
+  pr_mutual_inductive_body env sp mib ++
   with_line_skip
     (print_inductive_renames sp mipv @
      print_inductive_implicit_args sp mipv @
@@ -427,7 +427,6 @@ let print_constant with_values sep sp =
     | _ ->
 	print_basename sp ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ))
-  ++ fnl ()
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
@@ -442,7 +441,7 @@ let gallina_print_syntactic_def kn =
        (str "Notation " ++ pr_qualid qid ++
         prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
         spc () ++ str ":=") ++
-     spc () ++ Constrextern.without_symbols pr_glob_constr c) ++ fnl ()
+     spc () ++ Constrextern.without_symbols pr_glob_constr c)
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
@@ -675,17 +674,17 @@ let print_about_any k =
   match k with
   | Term ref ->
       pr_infos_list
-       ([print_ref false ref; blankline] @
+       (print_ref false ref :: blankline ::
 	print_name_infos ref @
 	print_simpl_behaviour ref @
 	print_opacity ref @
 	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
       v 0 (
-      print_syntactic_def kn ++
-      hov 0 (str "Expands to: " ++ pr_located_qualid k)) ++ fnl()
+      print_syntactic_def kn ++ fnl () ++
+      hov 0 (str "Expands to: " ++ pr_located_qualid k))
   | Dir _ | ModuleType _ | Undefined _ ->
-      hov 0 (pr_located_qualid k) ++ fnl()
+      hov 0 (pr_located_qualid k)
 
 let print_about = function
   | ByNotation (loc,ntn,sc) ->
@@ -763,7 +762,7 @@ let print_canonical_projections () =
 open Typeclasses
 
 let pr_typeclass env t =
-  print_ref false t.cl_impl ++ fnl ()
+  print_ref false t.cl_impl
 
 let print_typeclasses () =
   let env = Global.env () in
@@ -772,7 +771,7 @@ let print_typeclasses () =
 let pr_instance env i =
   (*   gallina_print_constant_with_infos i.is_impl *)
   (* lighter *)
-  print_ref false (instance_impl i) ++ fnl ()
+  print_ref false (instance_impl i)
 
 let print_all_instances () =
   let env = Global.env () in
diff --git a/printing/printer.ml b/printing/printer.ml
index d697ab9335..1e4ef47095 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -276,7 +276,7 @@ let default_pr_goal gs =
     str"  " ++ hv 0 (penv ++ fnl () ++
 		       str (emacs_str "")  ++
 		       str "============================" ++ fnl ()  ++
-		       thesis ++ str " " ++  pc) ++ fnl ()
+		       thesis ++ str " " ++  pc)
 
 (* display a goal tag *)
 let pr_goal_tag g =
@@ -312,13 +312,12 @@ let pr_evar (ev, evd) =
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int i = function
-  | [] -> (mt ())
+  | [] -> mt ()
   | (ev,evd)::rest ->
       let pegl = pr_evgl_sign evd in
-      let pei = pr_evars_int (i+1) rest in
       (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
               str (string_of_existential ev)  ++ str " : " ++ pegl)) ++
-      fnl () ++ pei
+      (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int (i+1) rest)
 
 let default_pr_subgoal n sigma =
   let rec prrec p = function
@@ -348,7 +347,7 @@ let emacs_print_dependent_evars sigma seeds =
 	    end i (str ",")
       end evars (str "")
     in
-    cut () ++
+    fnl () ++
     str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
   in
   delayed_emacs_cmd evars
@@ -361,11 +360,11 @@ let default_pr_subgoals close_cmd sigma seeds = function
 	match close_cmd with
 	  Some cmd ->
 	    (str "Subproof completed, now type " ++ str cmd ++
-	       str "." ++ fnl ())
+	       str ".")
 	| None ->
 	    let exl = Evarutil.non_instantiated sigma in
 	      if exl = [] then
-		(str"No more subgoals." ++ fnl ()
+		(str"No more subgoals."
 		 ++ emacs_print_dependent_evars sigma seeds)
 	      else
 		let pei = pr_evars_int 1 exl in
@@ -393,7 +392,7 @@ let default_pr_subgoals close_cmd sigma seeds = function
       v 0 (
 	int(List.length rest+1) ++ str" subgoals" ++
           str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
-	++ pg1 ++ prest ++ fnl ()
+	++ pg1 ++ prest
 	++ emacs_print_dependent_evars sigma seeds
       )
 
@@ -433,7 +432,7 @@ let pr_open_subgoals () =
             begin match bgoals with
 	    | [] -> pr_subgoals None sigma seeds goals
 	    | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++
-		      str"This subproof is complete, but there are still unfocused goals." ++ fnl ()
+		      str"This subproof is complete, but there are still unfocused goals."
 		(* spiwack: to stay compatible with the proof general and coqide,
 		    I use print the message after the goal. It would be better to have
 		    something like:
@@ -547,7 +546,7 @@ open Assumptions
 
 let pr_assumptionset env s =
   if ContextObjectMap.is_empty s then
-    str "Closed under the global context" ++ fnl()
+    str "Closed under the global context"
   else
     let safe_pr_constant env kn =
       try pr_constant env kn
@@ -567,7 +566,6 @@ let pr_assumptionset env s =
 			   ++ str (string_of_id id)
 			   ++ str " : "
 	                   ++ pr_ltype typ
-	                   ++ fnl ()
 			    )
 	                 ,
 	                   a, o)
@@ -576,7 +574,6 @@ let pr_assumptionset env s =
 			      Option.default (fnl ()) a
 			   ++ safe_pr_constant env kn
 	                   ++ safe_pr_ltype typ
-	                   ++ fnl ()
 			     )
 			 , o
 			 )
@@ -585,7 +582,6 @@ let pr_assumptionset env s =
 			      Option.default (fnl ()) o
 			   ++ safe_pr_constant env kn
 	                   ++ safe_pr_ltype typ
-	                   ++ fnl ()
 			     )
 			 )
       )