place all pretty-printing files in new dir printing/

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

24 files changed, 72 insertions, 80 deletions

diff --git a/Makefile.common b/Makefile.common
index d7325bcbb9..ea6a810dde 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -71,8 +71,8 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 SRCDIRS:=\
   config 	tools 		tools/coqdoc 	scripts		lib \
   kernel	kernel/byterun	library 	proofs 		tactics \
-  pretyping	interp		toplevel/utils	toplevel 	parsing 	\
-  grammar 	intf            ide/utils	ide		\
+  pretyping	interp		toplevel/utils	toplevel 	parsing \
+  printing	grammar 	intf            ide/utils	ide	\
   $(addprefix plugins/, \
     omega	romega 		micromega 	quote		ring \
     setoid_ring xml 		extraction 	fourier \
@@ -157,8 +157,8 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 
 CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
-        parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
-        parsing/highparsing.cma tactics/hightactics.cma
+        printing/printing.cma parsing/parsing.cma tactics/tactics.cma \
+	toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma
 
 GRAMMARCMA:=grammar/grammar.cma
 
@@ -346,7 +346,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 OCAMLDOCDIR=dev/ocamldoc
 
 DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
-	./pretyping/*.mli ./interp/*.mli \
+	./pretyping/*.mli ./interp/*.mli printing/*.mli \
 	./parsing/*.mli ./proofs/*.mli \
 	./tactics/*.mli ./toplevel/*.mli)
 
diff --git a/_tags b/_tags
index 19dfff544d..ca0d9e7b81 100644
--- a/_tags
+++ b/_tags
@@ -73,6 +73,7 @@
 "parsing": include
 "plugins": include
 "pretyping": include
+"printing": include
 "proofs": include
 "scripts": include
 "states": include
diff --git a/dev/base_include b/dev/base_include
index 1e692defb9..66d91f92e1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -12,7 +12,8 @@
 #directory "lib";;
 #directory "proofs";;
 #directory "tactics";;
-#directory "translate";;
+#directory "printing";;
+#directory "grammar";;
 #directory "intf";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 5358673ffe..1a55b804ea 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -12,7 +12,7 @@ OCAMLDEBUG=$CAMLBIN/ocamldebug
 exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
 	-I $COQTOP \
-	-I $COQTOP/config \
+	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
 	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index d73e80f113..98ba1f7621 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -5,9 +5,3 @@ Pcoq
 Egramml
 Egramcoq
 G_xml
-Ppconstr
-Printer
-Pptactic
-Tactic_printer
-Printmod
-Prettyp
diff --git a/parsing/ppconstr.ml b/printing/ppconstr.ml
index b64dd6ff87..2e3ce21037 100644
--- a/parsing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -10,7 +10,6 @@
 open Errors
 open Util
 open Pp
-open Nametab
 open Names
 open Nameops
 open Libnames
@@ -19,9 +18,6 @@ open Constrexpr
 open Constrexpr_ops
 open Topconstr
 open Term
-open Pattern
-open Constrextern
-open Termops
 open Decl_kinds
 open Misctypes
 open Locus
diff --git a/parsing/ppconstr.mli b/printing/ppconstr.mli
index 88e4e55dc6..6453c26f48 100644
--- a/parsing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -10,12 +10,8 @@ open Pp
 open Environ
 open Term
 open Libnames
-open Pcoq
-open Glob_term
 open Constrexpr
 open Names
-open Errors
-open Util
 open Misctypes
 open Locus
 open Genredexpr
diff --git a/printing/ppextra.ml b/printing/ppextra.ml
new file mode 100644
index 0000000000..a85cafd40c
--- /dev/null
+++ b/printing/ppextra.ml
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Ppextend
+open Pptactic
+open Extrawit
+
+let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
+
+let _ = for i=0 to 5 do
+  declare_extra_genarg_pprule
+  (rawwit_tactic i, pr_tac_polymorphic i)
+  (globwit_tactic i, pr_tac_polymorphic i)
+  (wit_tactic i, pr_tac_polymorphic i)
+done
diff --git a/parsing/pptactic.ml b/printing/pptactic.ml
index 15acfd718c..14cfe2ffcb 100644
--- a/parsing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -11,20 +11,18 @@ open Names
 open Namegen
 open Errors
 open Util
-open Tacexpr
-open Glob_term
 open Constrexpr
+open Tacexpr
 open Genarg
 open Libnames
-open Pattern
 open Ppextend
-open Ppconstr
-open Printer
 open Misctypes
 open Miscops
 open Locus
 open Decl_kinds
 open Genredexpr
+open Ppconstr
+open Printer
 
 let pr_global x = Nametab.pr_global_env Idset.empty x
 
@@ -728,7 +726,7 @@ and pr_atom1 = function
       hov 1
         (str "double induction" ++
          pr_arg pr_quantified_hypothesis h1 ++
- 	 pr_arg pr_quantified_hypothesis h2)
+	 pr_arg pr_quantified_hypothesis h2)
   | TacDecomposeAnd c ->
       hov 1 (str "decompose record" ++ pr_constrarg c)
   | TacDecomposeOr c ->
@@ -1046,17 +1044,5 @@ let _ = Tactic_debug.set_match_pattern_printer
 
 let _ = Tactic_debug.set_match_rule_printer
   (fun rl ->
-    pr_match_rule false (pr_glob_tactic (Global.env())) 
+    pr_match_rule false (pr_glob_tactic (Global.env()))
       (fun (_,p) -> pr_constr_pattern p) rl)
-
-open Extrawit
-
-let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
-
-let _ = for i=0 to 5 do
-  declare_extra_genarg_pprule
-  (rawwit_tactic i, pr_tac_polymorphic i)
-  (globwit_tactic i, pr_tac_polymorphic i)
-  (wit_tactic i, pr_tac_polymorphic i)
-done
-
diff --git a/parsing/pptactic.mli b/printing/pptactic.mli
index 7a5c435315..58b45152c6 100644
--- a/parsing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -8,15 +8,12 @@
 
 open Pp
 open Genarg
+open Constrexpr
 open Tacexpr
-open Pretyping
 open Proof_type
-open Constrexpr
-open Glob_term
-open Pattern
 open Ppextend
 open Environ
-open Evd
+open Pattern
 open Misctypes
 
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
diff --git a/parsing/ppvernac.ml b/printing/ppvernac.ml
index b8782c67c3..9a8bf3c38b 100644
--- a/parsing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -406,7 +406,7 @@ let make_pr_vernac pr_constr pr_lconstr =
 let pr_constrarg c = spc () ++ pr_constr c in
 let pr_lconstrarg c = spc () ++ pr_lconstr c in
 let pr_intarg n = spc () ++ int n in
-let pr_oc = function 
+let pr_oc = function
     None -> str" :"
   | Some true -> str" :>"
   | Some false -> str" :>>"
@@ -491,7 +491,7 @@ let rec pr_vernac = function
   (* Syntax *)
   | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e)
   | VernacOpenCloseScope (local,opening,sc) ->
-      pr_section_locality local ++ 
+      pr_section_locality local ++
       str (if opening then "Open " else "Close ") ++
       str "Scope" ++ spc() ++ str sc
   | VernacDelimiters (sc,key) ->
@@ -503,7 +503,7 @@ let rec pr_vernac = function
   | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
       |	None -> str"_"
       |	Some sc -> str sc in
-    pr_section_locality local ++ str"Arguments Scope" ++ spc() ++ 
+    pr_section_locality local ++ str"Arguments Scope" ++ spc() ++
     pr_smart_global q
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
   | VernacInfix (local,((_,s),mv),q,sn) -> (* A Verifier *)
@@ -663,11 +663,11 @@ let rec pr_vernac = function
      hov 1 (
        pr_non_locality (not glob) ++
        (if abst then str"Declare " else mt ()) ++
-       str"Instance" ++ 
-       (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | 
+       str"Instance" ++
+       (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
 	Anonymous -> mt ()) ++
        pr_and_type_binders_arg sup ++
-       str":" ++ spc () ++	 
+       str":" ++ spc () ++
        pr_constr_expr cl ++ spc () ++
 	 (match props with
 	  | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr_expr p
@@ -760,11 +760,11 @@ let rec pr_vernac = function
         (pr_locality local ++ str "Ltac " ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacCreateHintDb (local,dbname,b) ->
-      hov 1 (pr_locality local ++ str "Create HintDb " ++ 
+      hov 1 (pr_locality local ++ str "Create HintDb " ++
 		str dbname ++ (if b then str" discriminated" else mt ()))
   | VernacRemoveHints (local, dbnames, ids) ->
       hov 1 (pr_locality local ++ str "Remove Hints " ++
-	       prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ 
+	       prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
 	       pr_opt_hintbases dbnames)
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_constr_pattern_expr
@@ -774,10 +774,10 @@ let rec pr_vernac = function
 	 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,[]) ->
-      hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ 
+      hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++
 	pr_smart_global q)
   | VernacDeclareImplicits (local,q,impls) ->
-      hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ 
+      hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++
 	spc() ++ pr_smart_global q ++ spc() ++
 	prlist_with_sep spc (fun imps ->
 	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
diff --git a/parsing/ppvernac.mli b/printing/ppvernac.mli
index 91bb19a8c6..91bb19a8c6 100644
--- a/parsing/ppvernac.mli
+++ b/printing/ppvernac.mli
diff --git a/parsing/prettyp.ml b/printing/prettyp.ml
index f4c53333fc..7bd41cc221 100644
--- a/parsing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -26,13 +26,13 @@ open Environ
 open Declare
 open Impargs
 open Libobject
-open Printer
-open Printmod
 open Libnames
 open Globnames
 open Nametab
 open Recordops
 open Misctypes
+open Printer
+open Printmod
 
 type object_pr = {
   print_inductive           : mutual_inductive -> std_ppcmds;
@@ -440,7 +440,7 @@ let gallina_print_syntactic_def kn =
   hov 2
     (hov 4
        (str "Notation " ++ pr_qualid qid ++
-        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ 
+        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
         spc () ++ str ":=") ++
      spc () ++ Constrextern.without_symbols pr_glob_constr c) ++ fnl ()
 
@@ -783,4 +783,3 @@ let print_instances r =
   let env = Global.env () in
   let inst = instances r in
     prlist_with_sep fnl (pr_instance env) inst
-
diff --git a/parsing/prettyp.mli b/printing/prettyp.mli
index d6bec71625..dfd15a6d16 100644
--- a/parsing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 open Sign
 open Term
diff --git a/parsing/printer.ml b/printing/printer.ml
index 8754b9129f..1c51a67558 100644
--- a/parsing/printer.ml
+++ b/printing/printer.ml
@@ -23,9 +23,9 @@ open Evd
 open Proof_type
 open Refiner
 open Pfedit
-open Ppconstr
 open Constrextern
 open Tacexpr
+open Ppconstr
 
 open Store.Field
 
@@ -324,11 +324,11 @@ let default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
     | g::rest ->
-       	if p = 1 then
+	if p = 1 then
           let pg = default_pr_goal { sigma=sigma ; it=g } in
           v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
 	       ++ str " is:" ++ cut () ++ pg)
-       	else
+	else
 	  prrec (p-1) rest
   in
   prrec n
@@ -348,7 +348,7 @@ let emacs_print_dependent_evars sigma seeds =
 	    end i (str ",")
       end evars (str "")
     in
-    cut () ++ 
+    cut () ++
     str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
   in
   delayed_emacs_cmd evars
@@ -437,7 +437,7 @@ let pr_open_subgoals () =
 		(* 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:
- 		      str"This subproof is complete, but there are still unfocused goals:" 
+		      str"This subproof is complete, but there are still unfocused goals:"
 		      ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals
 		    instead. But it doesn't quite work.
 		*)
@@ -453,7 +453,7 @@ let pr_nth_open_subgoal n =
 let pr_goal_by_id id =
   let p = Proof_global.give_me_the_proof () in
   let g = Goal.get_by_uid id in
-  let pr gs = 
+  let pr gs =
     v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
 	 ++ pr_goal gs)
   in
@@ -604,9 +604,9 @@ let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
 
 open Typeclasses
 
-let pr_instance i = 
+let pr_instance i =
   pr_global (instance_impl i)
-    
+
 let pr_instance_gmap insts =
   prlist_with_sep fnl (fun (gr, insts) ->
     prlist_with_sep fnl pr_instance (cmap_to_list insts))
diff --git a/parsing/printer.mli b/printing/printer.mli
index 77e4db79e1..3b9ef8ecc0 100644
--- a/parsing/printer.mli
+++ b/printing/printer.mli
@@ -115,7 +115,7 @@ val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
 
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
-(** Emacs/proof general support 
+(** Emacs/proof general support
    (emacs_str s) outputs
     - s if emacs mode,
     - nothing otherwise.
diff --git a/printing/printing.mllib b/printing/printing.mllib
new file mode 100644
index 0000000000..f7fbe4e138
--- /dev/null
+++ b/printing/printing.mllib
@@ -0,0 +1,6 @@
+Ppconstr
+Printer
+Pptactic
+Tactic_printer
+Printmod
+Prettyp
\ No newline at end of file
diff --git a/parsing/printmod.ml b/printing/printmod.ml
index d81802ac2e..1953935aab 100644
--- a/parsing/printmod.ml
+++ b/printing/printmod.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open Errors
-open Util
 open Names
 open Declarations
 open Nameops
diff --git a/parsing/printmod.mli b/printing/printmod.mli
index a45bdb9851..348d88bf5a 100644
--- a/parsing/printmod.mli
+++ b/printing/printmod.mli
@@ -6,12 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 
 (** false iff the module is an element of an open module type *)
 val printable_body : dir_path -> bool
 
-val print_module : bool -> module_path -> std_ppcmds
+val print_module : bool -> module_path -> Pp.std_ppcmds
 
-val print_modtype : module_path -> std_ppcmds
+val print_modtype : module_path -> Pp.std_ppcmds
diff --git a/parsing/tactic_printer.ml b/printing/tactic_printer.ml
index b2b59f1660..2c51abcd01 100644
--- a/parsing/tactic_printer.ml
+++ b/printing/tactic_printer.ml
@@ -13,7 +13,6 @@ open Sign
 open Evd
 open Tacexpr
 open Proof_type
-open Logic
 open Printer
 
 let pr_tactic = function
@@ -62,7 +61,7 @@ let rec print_proof sigma osign pf =
     | None ->
 	hov 0 (pr_goal {sigma = sigma; it=pf.goal })
     | Some(r,spfl) ->
-    	hov 0
+	hov 0
 	  (hov 0 (pr_goal {sigma = sigma; it=pf.goal }) ++
 	   spc () ++ str" BY " ++
 	   hov 0 (pr_rule r) ++ fnl () ++
@@ -169,5 +168,3 @@ let rec print_info_script sigma osign pf =
 
 let format_print_info_script sigma osign pf =
   hov 0 (print_info_script sigma osign pf)
-
-
diff --git a/parsing/tactic_printer.mli b/printing/tactic_printer.mli
index 5ea579107f..5ea579107f 100644
--- a/parsing/tactic_printer.mli
+++ b/printing/tactic_printer.mli
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 5105ac6c90..f38eed4c77 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -365,8 +365,9 @@ let variables is_install opt (args,defs) =
     print "COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \\
   -I $(COQLIB)library -I $(COQLIB)parsing \\
   -I $(COQLIB)pretyping -I $(COQLIB)interp \\
+  -I $(COQLIB)printing -I $(COQLIB)intf \\
   -I $(COQLIB)proofs -I $(COQLIB)tactics \\
-  -I $(COQLIB)toplevel";
+  -I $(COQLIB)toplevel -I $(COQLIB)grammar";
     List.iter (fun c -> print " \\
   -I $(COQLIB)plugins/"; print c) Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 15916ef8cc..02cf8ffe49 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -134,4 +134,5 @@ let init_ocaml_path () =
     List.iter add_subdir
       [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
 	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
-	[ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
+	[ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ];
+        [ "grammar" ]; [ "ide" ] ]
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 43d15eb434..56c79eddac 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -13,6 +13,7 @@ Obligations
 Command
 Classes
 Record
+Ppextra
 Ppvernac
 Backtrack
 Vernacinterp