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

5 files changed, 38 insertions, 39 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 ()
 			     )
 			 )
       )
diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
index b1883ec060..1292123b19 100644
--- a/test-suite/output/Nametab.out
+++ b/test-suite/output/Nametab.out
@@ -7,11 +7,11 @@ Constant Top.Q.N.K.foo
 Constant Top.Q.N.K.foo
 Constant Top.Q.N.K.foo
   (shorter name to refer to it in current context is Q.N.K.foo)
-No module is referred to by basename K
-No module is referred to by name N.K
+Error: No module is referred to by basename K
+Error: No module is referred to by name N.K
 Module Top.Q.N.K
 Module Top.Q.N.K
-No module is referred to by basename N
+Error: No module is referred to by basename N
 Module Top.Q.N
 Module Top.Q.N
 Module Top.Q
@@ -26,10 +26,10 @@ Constant Top.Q.N.K.foo
 Constant Top.Q.N.K.foo
   (shorter name to refer to it in current context is K.foo)
 Module Top.Q.N.K
-No module is referred to by name N.K
+Error: No module is referred to by name N.K
 Module Top.Q.N.K
 Module Top.Q.N.K
-No module is referred to by basename N
+Error: No module is referred to by basename N
 Module Top.Q.N
 Module Top.Q.N
 Module Top.Q
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 9106a4e368..d546f84daa 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -14,6 +14,7 @@ minus: nat -> nat -> nat
 min: nat -> nat -> nat
 max: nat -> nat -> nat
 length: forall A : Type, list A -> nat
+
 S: nat -> nat
 pred: nat -> nat
 plus: nat -> nat -> nat
@@ -28,3 +29,4 @@ eq_refl: forall (A : Type) (x : A), x = x
 iff_refl: forall A : Prop, A <-> A
 pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
+
diff --git a/toplevel/search.ml b/toplevel/search.ml
index fbfa83d08b..520b74ada7 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -113,7 +113,9 @@ let xor a b = (a or b) & (not (a & b))
 let plain_display accu ref a c =
   let pc = pr_lconstr_env a c in
   let pr = pr_global ref in
-  accu := !accu ++ hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()
+  accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu
+
+let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
 
 let filter_by_module (module_list:dir_path list) (accept:bool)
   (ref:global_reference) _ _ =
@@ -197,19 +199,19 @@ let raw_search search_function extra_filter display_function pat =
     ) (search_function pat)
 
 let text_pattern_search extra_filter pat =
-  let ans = ref (mt ()) in
+  let ans = ref [] in
   raw_search Libtypes.search_concl extra_filter (plain_display ans) pat;
-  !ans
+  format_display !ans
 
 let text_search_rewrite extra_filter pat =
-  let ans = ref (mt ()) in
+  let ans = ref [] in
   raw_search (Libtypes.search_eq_concl c_eq) extra_filter (plain_display ans) pat;
-  !ans
+  format_display !ans
 
 let text_search_by_head extra_filter pat =
-  let ans = ref (mt ()) in
+  let ans = ref [] in
   raw_search Libtypes.search_head_concl extra_filter (plain_display ans) pat;
-  !ans
+  format_display !ans
 
 let filter_by_module_from_list = function
   | [], _ -> (fun _ _ _ -> true)
@@ -254,6 +256,6 @@ let raw_search_about filter_modules display_function l =
   gen_filtered_search filter display_function
 
 let search_about reference inout =
-  let ans = ref (mt ()) in
+  let ans = ref [] in
   raw_search_about (filter_by_module_from_list inout) (plain_display ans) reference;
-  !ans
+  format_display !ans