Merge PR#582: Fix warnings

11 files changed, 10 insertions, 33 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index c91dcc505..f363deac6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -9,7 +9,6 @@
 (* This file is about the automatic generation of schemes about
    decidable equality, created by Vincent Siles, Oct 2007 *)
 
-open Tacmach
 open CErrors
 open Util
 open Pp
@@ -28,8 +27,6 @@ open Proofview.Notations
 
 module RelDecl = Context.Rel.Declaration
 
-let out_punivs = Univ.out_punivs
-
 (**********************************************************************)
 (* Generic synthesis of boolean equality *)
 
@@ -718,7 +715,6 @@ let compute_lb_goal ind lnamesparrec nparrec =
         ))), eff
 
 let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
-  let open EConstr in
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
       let first_intros =
diff --git a/vernac/class.ml b/vernac/class.ml
index 95114ec39..104f3c1db 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -311,7 +311,7 @@ let add_coercion_hook poly local ref =
   | Global -> false
   | Discharge -> assert false
   in
-  let () = try_add_new_coercion ref stre poly in
+  let () = try_add_new_coercion ref ~local:stre poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
@@ -324,6 +324,6 @@ let add_subclass_hook poly local ref =
   | Discharge -> assert false
   in
   let cl = class_of_global ref in
-  try_add_new_coercion_subclass cl stre poly
+  try_add_new_coercion_subclass cl ~local:stre poly
 
 let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 833719965..d515b0c9b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -66,8 +66,6 @@ let _ =
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
 
-open Vernacexpr
-
 (** TODO: add subinstances *)
 let existing_instance glob g info =
   let c = global g in
diff --git a/vernac/command.ml b/vernac/command.ml
index 3ea8f6590..2fa2aa4e3 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -258,7 +258,7 @@ match local with
   let () = Universes.register_universe_binders gr pl in
   let () = assumption_message ident in
   let () = Typeclasses.declare_instance None false gr in
-  let () = if is_coe then Class.try_add_new_coercion gr local p in
+  let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = 
     if p (* polymorphic *) then Univ.UContext.instance ctx 
     else Univ.Instance.empty
@@ -752,7 +752,7 @@ let do_mutual_inductive indl poly prv finite =
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes;
+  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index 85d0b6194..c6588684a 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -151,7 +151,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let const = define mode id c mib.mind_polymorphic ctx in
   declare_scheme kind [|ind,const|];
   const, Safe_typing.add_private
-     (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff
+     (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -172,7 +172,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
   consts,
   Safe_typing.add_private 
     (Safe_typing.private_con_of_scheme
-      kind (Global.safe_env()) (Array.to_list schemes))
+      ~kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
 let define_mutual_scheme kind mode names mind =
@@ -185,7 +185,7 @@ let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
   s, Safe_typing.add_private
       (Safe_typing.private_con_of_scheme
-            kind (Global.safe_env()) [ind, s])
+            ~kind (Global.safe_env()) [ind, s])
       Safe_typing.empty_private_constants
 
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f805eeaa9..bb5be4cb0 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -527,7 +527,7 @@ let warn_skip_spaces_curly =
       (fun () ->strbrk "Skipping spaces inside curly brackets")
 
 let rec drop_spacing = function
-  | UnpCut _ as u :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt
+  | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt
   | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt
   | fmt -> fmt
 
@@ -1196,7 +1196,7 @@ let inNotation : notation_obj -> obj =
 (**********************************************************************)
 
 let with_lib_stk_protection f x =
-  let fs = Lib.freeze `No in
+  let fs = Lib.freeze ~marshallable:`No in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
     let reraise = CErrors.push reraise in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 11366fe91..a276f9f9a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -12,7 +12,6 @@ open Evd
 open Names
 open Pp
 open Globnames
-open Vernacexpr
 open Decl_kinds
 
 (** Forward declaration. *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 8b4b7606f..53722b8f6 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -216,7 +216,7 @@ let warning_or_error coe indsp err =
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then user_err ~hdr:"structure" st;
-  Flags.if_verbose Feedback.msg_info (hov 0 st)
+  warn_cannot_define_projection (hov 0 st)
 
 type field_status =
   | NoProjection of Name.t
diff --git a/vernac/search.ml b/vernac/search.ml
index 6279b17ae..5b6e9a9c3 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -14,11 +14,9 @@ open Declarations
 open Libobject
 open Environ
 open Pattern
-open Printer
 open Libnames
 open Globnames
 open Nametab
-open Goptions
 
 module NamedDecl = Context.Named.Declaration
 
diff --git a/vernac/search.mli b/vernac/search.mli
index 82b79f75d..e34522d8a 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Environ
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index a1835959c..6d9d71a62 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -106,8 +106,6 @@ module Tag = struct
 
 end
 
-type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
-
 let msgnl_with ?pre_hdr fmt strm =
   pp_with fmt (strm ++ fnl ());
   Format.pp_print_flush fmt ()
@@ -133,7 +131,6 @@ let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
 let info_hdr = mt ()
 let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
 let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
-let  ann_hdr = tag Tag.error   (str "Anomaly:") ++ spc ()
 
 let make_body quoter info ?pre_hdr s =
   pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s))
@@ -283,16 +280,6 @@ let print_err_exn ?extra any =
   let msg = CErrors.iprint (e, info) ++ fnl () in
   std_logger ~pre_hdr Feedback.Error msg
 
-(* Output to file, used only in extraction so a candidate for removal *)
-let ft_logger old_logger ft ?loc level mesg =
-  let id x = x in
-  match level with
-  | Debug   -> msgnl_with ft (make_body id  dbg_hdr mesg)
-  | Info    -> msgnl_with ft (make_body id info_hdr mesg)
-  | Notice  -> msgnl_with ft mesg
-  | Warning -> old_logger ?loc level mesg
-  | Error   -> old_logger ?loc level mesg
-
 let with_output_to_file fname func input =
   (* XXX FIXME: redirect std_ft  *)
   (* let old_logger = !logger in *)