Print Assumptions est pret pour la release.

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

3 files changed, 37 insertions, 26 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index ac21550983..6bd11af9f6 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -468,32 +468,46 @@ let pr_prim_rule = function
 let prterm = pr_lconstr
 
 
-(* spiwack a little printer function for sets of Environ.assumption *)
-(* arnaud : tester "Print Assumptions" *)
+(* spiwack: printer function for sets of Environ.assumption.
+            It is used primarily by the Print Assumption command. *)
+exception EmptyAssumptionSet
+
 let pr_assumptionset env s = 
-  if not (Environ.AssumptionSet.is_empty s) then
+  if (Environ.AssumptionSet.is_empty s) then
+    str "Closed under the global context"
+  else
     let (vars, axioms) = Environ.AssumptionSet.partition 
-                         (function |Variable _ -> true | _ -> false) s
+                         (function |Variable _ -> true | _ -> false) 
+			 s
     in
-    (if not (Environ.AssumptionSet.is_empty vars) then
-      str "Section Variables:" ++ fnl () ++
+    (if Environ.AssumptionSet.is_empty vars then
+       mt ()
+     else
+      str "Section Variables:" ++
       (Environ.AssumptionSet.fold 
          (function Variable (id,typ ) -> 
-	    (fun s -> s++str (string_of_identifier id)++str " : "++pr_ltype typ++spc ())
-	    | _ -> assert false)
+	    (fun b -> b++str (string_of_identifier id)
+	               ++str " : "
+	               ++pr_ltype typ
+	               ++fnl ())
+	 | _ -> anomaly 
+	        "Printer.pr_assumptionset: failure of partition (Variable)")
          vars (fnl ()))
-     else
-       mt ()
-    )++
-    if not (Environ.AssumptionSet.is_empty axioms) then
-      str "Axioms:" ++ fnl () ++
+    )
+    ++ fnl () 
+    ++
+    if Environ.AssumptionSet.is_empty axioms then
+      mt ()
+    else
+      str "Axioms:" ++
       (Environ.AssumptionSet.fold
          (function Axiom (cst, typ) -> 
-	    (fun s -> s++(pr_constant env cst)++str " : "++pr_ltype typ++spc ())
-	    | _ -> assert false)
-         axioms (mt ()))
-    else
-      mt ()
-  else
-    raise Not_found
+	    (fun b -> b++(pr_constant env cst)
+	               ++str " : "
+	               ++pr_ltype typ
+	               ++fnl ())
+	  | _ -> anomaly 
+	         "Printer.pr_assumptionset: failure of partition (Axiom)")
+         axioms 
+	 (fnl ()))
 
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 1f3f2b0fbf..0e25f1bd0d 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -115,7 +115,8 @@ val emacs_str              : string -> string -> string
 val prterm                 : constr -> std_ppcmds (* = pr_lconstr *)
 
 
-(* spiwack: A printer for sets of Environ.assumption *)
+(* spiwack: printer function for sets of Environ.assumption.
+            It is used primarily by the Print Assumption command. *)
 val pr_assumptionset : env -> Environ.AssumptionSet.t -> std_ppcmds
 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cb9e953568..b71f9767ef 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -970,11 +970,7 @@ let vernac_print = function
   | PrintAssumptions r ->
       let cstr = constr_of_global (global_with_alias r) in
       let nassumptions = Environ.assumptions cstr (Global.env ()) in
-      msg 
-      (try
-        Printer.pr_assumptionset (Global.env ()) nassumptions
-      with Not_found ->
-        pr_reference r ++ str " is closed under the global context")
+      msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in