Remove some more "open" and dead code thanks to OCaml4 warnings

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

5 files changed, 5 insertions, 15 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 190181c23..1d03716d0 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -17,7 +17,6 @@ open Ppextend
 open Constrexpr
 open Constrexpr_ops
 open Topconstr
-open Term
 open Decl_kinds
 open Misctypes
 open Locus
@@ -34,7 +33,6 @@ let lif = 200
 let lletin = 200
 let lletpattern = 200
 let lfix = 200
-let larrow = 90
 let lcast = 100
 let larg = 9
 let lapp = 10
@@ -612,7 +610,6 @@ let pr_red_flag pr r =
      pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
      hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
 
-
 let pr_metaid id = str"?" ++ pr_id id
 
 let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 8bdea1356..d16035fba 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -220,7 +220,6 @@ let rec pr_glob_generic prc prlc prtac prpat x =
       try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
-
 let rec pr_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen wit_bool x then "true" else "false")
@@ -549,7 +548,6 @@ let linfo = 5
 
 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 
-
 (** A printer for tactics that polymorphically works on the three
     "raw", "glob" and "typed" levels; in practice, the environment is
     used only at the glob and typed level: it is used to feed the
diff --git a/printing/printer.ml b/printing/printer.ml
index 374b5d597..74c5a02d5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -22,7 +22,6 @@ open Pfedit
 open Constrextern
 open Ppconstr
 
-
 let emacs_str s =
   if !Flags.print_emacs then s else ""
 let delayed_emacs_cmd s =
diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml
index e347b6c89..87bb89e8d 100644
--- a/printing/tactic_printer.ml
+++ b/printing/tactic_printer.ml
@@ -51,8 +51,6 @@ let pr_rule_dot_fnl = function
    | Prim Change_evars -> mt ()
    | r -> pr_rule_dot r ++ fnl ()
 
-exception Different
-
 let rec print_proof sigma osign pf =
   (* spiwack: [osign] is currently ignored, not sure if this function is even used. *)
   let hyps = Environ.named_context_of_val (Goal.V82.hyps sigma pf.goal) in
diff --git a/printing/tactic_printer.mli b/printing/tactic_printer.mli
index 1c045e624..e94a2a771 100644
--- a/printing/tactic_printer.mli
+++ b/printing/tactic_printer.mli
@@ -6,18 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Sign
 open Evd
-open Tacexpr
 open Proof_type
 
 (** These are the entry points for tactics, proof trees, ... *)
 
-val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
-val pr_rule     : rule -> std_ppcmds
-val pr_tactic   : tactic_expr -> std_ppcmds
+val print_proof : evar_map -> named_context -> proof_tree -> Pp.std_ppcmds
+val pr_rule     : rule -> Pp.std_ppcmds
+val pr_tactic   : tactic_expr -> Pp.std_ppcmds
 val print_script :
-  ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
+  ?nochange:bool -> evar_map -> proof_tree -> Pp.std_ppcmds
 val print_treescript :
-  ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
+  ?nochange:bool -> evar_map -> proof_tree -> Pp.std_ppcmds