Fixing Print Assumption display

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

1 files changed, 26 insertions, 36 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index a59800a9c1..d95ccef896 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -578,44 +578,34 @@ let pr_assumptionset env s =
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ with _ -> mt ()
     in
-    let (vars,axioms,opaque) =
-      ContextObjectMap.fold (fun t typ r ->
-	let (v,a,o) = r in
-	match t with
-	| Variable id -> (  Some (
-	                      Option.default (fnl ()) v
-			   ++ str (string_of_id id)
-			   ++ str " : "
-	                   ++ pr_ltype typ
-			    )
-	                 ,
-	                   a, o)
-	| Axiom kn    -> ( v ,
-			     Some (
-			      Option.default (fnl ()) a
-			   ++ safe_pr_constant env kn
-	                   ++ safe_pr_ltype typ
-			     )
-			 , o
-			 )
-	| Opaque kn    -> ( v , a ,
-			     Some (
-			      Option.default (fnl ()) o
-			   ++ safe_pr_constant env kn
-	                   ++ safe_pr_ltype typ
-			     )
-			 )
-      )
-	s (None,None,None)
+    let fold t typ accu =
+      let (v, a, o) = accu in
+      match t with
+      | Variable id ->
+        let var = str (string_of_id id) ++ str " : " ++ pr_ltype typ in
+        (var :: v, a, o)
+      | Axiom kn ->
+        let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        (v, ax :: a, o)
+      | Opaque kn ->
+        let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        (v, a, opq :: o)
     in
-    let (vars,axioms,opaque) =
-      ( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
-	Option.map (fun p -> str "Axioms:" ++ p) axioms ,
-	Option.map (fun p -> str "Opaque constants:" ++ p) opaque
-      )
+    let (vars, axioms, opaque) = ContextObjectMap.fold fold s ([], [], []) in
+    let opt_list title = function
+    | [] -> None
+    | l ->
+      let section =
+        title ++ fnl () ++
+        v 0 (prlist_with_sep fnl (fun s -> s) l) in
+      Some section
     in
-    (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
-      ++ (Option.default (mt ()) opaque)
+    let assums = [
+      opt_list (str "Section Variables:") vars;
+      opt_list (str "Axioms:") axioms;
+      opt_list (str "Opaque constants:") opaque;
+    ] in
+    prlist_with_sep fnl (pr_opt_no_spc (fun x -> x)) assums
 
 let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []