Merge PR#582: Fix warnings

5 files changed, 1 insertions, 15 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 38eeda9b96..3041ac259e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -212,10 +212,6 @@ let tag_var = tag Tag.variable
       | Some (_,ExplByName id) ->
         str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
 
-  let pr_opt_type pr = function
-    | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
-    | t -> cut () ++ str ":" ++ pr t
-
   let pr_opt_type_spc pr = function
     | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f0c8cd58c1..3e41439c8c 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -394,10 +394,6 @@ open Decl_kinds
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
          str":" ++ pr_spc_lconstr c)
 
-  let pr_priority = function
-    | None -> mt ()
-    | Some i -> spc () ++ str "|" ++ spc () ++ int i
-
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index aa422e36af..381af83c73 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -29,7 +29,7 @@ open Printer
 open Printmod
 open Context.Rel.Declaration
 
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 38e1110344..6841781ccd 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -8,7 +8,6 @@
 
 open Pp
 open Names
-open Term
 open Environ
 open Reductionops
 open Libnames
diff --git a/printing/printer.ml b/printing/printer.ml
index 35ddf2e8cf..93d221f03f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -370,11 +370,6 @@ let pr_context_limit_compact ?n env sigma =
       env ~init:(mt ()) in
   (sign_env ++ db_env)
 
-(* compact printing an env (variables and de Bruijn). Separator: three
-   spaces between simple hyps, and newline otherwise *)
-let pr_context_unlimited_compact env sigma =
-  pr_context_limit_compact env sigma
-
 (* The number of printed hypothesis in a goal *)
 (* If [None], no limit *)
 let print_hyps_limit = ref (None : int option)