Déplacement de pr_arg et pr_opt de Ppconstr vers Util

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

4 files changed, 5 insertions, 9 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 476725a91a..df5be249d7 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -694,6 +694,8 @@ let pr_str = str
 let pr_coma () = str "," ++ spc ()
 let pr_semicolon () = str ";" ++ spc ()
 let pr_bar () = str "|" ++ spc ()
+let pr_arg pr x = spc () ++ pr x
+let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 
 let pr_ord n =
   let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
diff --git a/lib/util.mli b/lib/util.mli
index 45e953a649..3993fc8519 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -223,6 +223,8 @@ val pr_coma : unit -> std_ppcmds
 val pr_semicolon : unit -> std_ppcmds
 val pr_bar : unit -> std_ppcmds
 val pr_ord : int -> std_ppcmds
+val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
+val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 5a969490d9..8bf2f42075 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -111,10 +111,6 @@ let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
 
 let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
-let pr_opt pr = function
-  | None -> mt ()
-  | Some x -> spc() ++ pr x
-
 let pr_optc pr = function
   | None -> mt ()
   | Some x -> pr_sep_com spc pr x
@@ -397,8 +393,6 @@ let pr_recursive pr_decl id = function
         (pr_decl true) dl ++
       fnl() ++ str "for " ++ pr_id id
 
-let pr_arg pr x = spc () ++ pr x
-
 let is_var id = function
   | CRef (Ident (_,id')) when id=id' -> true
   | _ -> false
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 51fbfcb262..ecfa5b4f33 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -35,9 +35,7 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool
  
 val pr_tight_coma : unit -> std_ppcmds
 
-val pr_located :
-  ('a -> std_ppcmds) -> 'a located -> std_ppcmds
-val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
 val pr_metaid : identifier -> std_ppcmds