Merge PR#582: Fix warnings

7 files changed, 10 insertions, 49 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 6d259e1b1..462905808 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -99,7 +99,6 @@ module Error = struct
     | Unterminated_string
     | Undefined_token
     | Bad_token of string
-    | UnsupportedUnicode of int
 
   exception E of t
 
@@ -110,12 +109,7 @@ module Error = struct
          | Unterminated_comment -> "Unterminated comment"
          | Unterminated_string -> "Unterminated string"
          | Undefined_token -> "Undefined token"
-         | Bad_token tok -> Format.sprintf "Bad token %S" tok
-         | UnsupportedUnicode x ->
-             Printf.sprintf "Unsupported Unicode character (0x%x)" x)
-
-  (* Require to fix the Camlp4 signature *)
-  let print ppf x = Pp.pp_with ppf (Pp.str (to_string x))
+         | Bad_token tok -> Format.sprintf "Bad token %S" tok)
 
 end
 open Error
@@ -153,10 +147,6 @@ let bump_loc_line_last loc bol_pos =
   in
   Ploc.encl loc loc'
 
-let set_loc_file loc fname =
-  Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc)
-		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
-
 (* For some reason, the [Ploc.after] function of Camlp5 does not update line
    numbers, so we define our own function that does it. *)
 let after loc =
@@ -345,13 +335,13 @@ let rec string loc ~comm_level bp len = parser
       if esc then string loc ~comm_level bp (store len '"') s else (loc, len)
   | [< ''('; s >] ->
       (parser
-        | [< ''*'; s >] ->
-            string loc
-              (Option.map succ comm_level)
+      | [< ''*'; s >] ->
+        let comm_level = Option.map succ comm_level in
+            string loc ~comm_level
               bp (store (store len '(') '*')
               s
         | [< >] ->
-            string loc comm_level bp (store len '(') s) s
+            string loc ~comm_level bp (store len '(') s) s
   | [< ''*'; s >] ->
       (parser
         | [< '')'; s >] ->
@@ -361,9 +351,9 @@ let rec string loc ~comm_level bp len = parser
             | _ -> ()
             in
             let comm_level = Option.map pred comm_level in
-            string loc comm_level bp (store (store len '*') ')') s
+            string loc ~comm_level bp (store (store len '*') ')') s
         | [< >] ->
-            string loc comm_level bp (store len '*') s) s
+            string loc ~comm_level bp (store len '*') s) s
   | [< ''\n' as c; s >] ep ->
      (* If we are parsing a comment, the string if not part of a token so we
      update the first line of the location. Otherwise, we update the last
@@ -372,8 +362,8 @@ let rec string loc ~comm_level bp len = parser
        if Option.has_some comm_level then bump_loc_line loc ep
        else bump_loc_line_last loc ep
      in
-     string loc comm_level bp (store len c) s
-  | [< 'c; s >] -> string loc comm_level bp (store len c) s
+     string loc ~comm_level bp (store len c) s
+  | [< 'c; s >] -> string loc ~comm_level bp (store len c) s
   | [< _ = Stream.empty >] ep ->
      let loc = set_loc_pos loc bp ep in
      err loc Unterminated_string
@@ -434,7 +424,6 @@ let push_char c =
     real_push_char c
 
 let push_string s = Buffer.add_string current_comment s
-let push_bytes s = Buffer.add_bytes current_comment s
 
 let null_comment s =
   let rec null i =
@@ -613,7 +602,7 @@ let rec next_token loc = parser bp
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
       comment_stop bp;
       (INT (get_buff len), set_loc_pos loc bp ep)
-  | [< ''\"'; (loc,len) = string loc None bp 0 >] ep ->
+  | [< ''\"'; (loc,len) = string loc ~comm_level:None bp 0 >] ep ->
       comment_stop bp;
       (STRING (get_buff len), set_loc_pos loc bp ep)
   | [< ' ('(' as c);
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 496b20002..86c66ec5f 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Pcoq
 open Constrexpr
-open Notation
 open Notation_term
 open Extend
 open Libnames
@@ -80,10 +79,6 @@ let create_pos = function
   | None -> Extend.First
   | Some lev -> Extend.After (constr_level lev)
 
-type gram_level =
-  gram_position option * gram_assoc option * string option *
-  (** for reinitialization: *) gram_reinit option
-
 let find_position_gen current ensure assoc lev =
   match lev with
   | None ->
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 6dda3817a..0a0430ba6 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -6,14 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Constrexpr
-open Notation_term
-open Pcoq
-open Extend
-open Genarg
-open Egramml
-
 (** Mapping of grammar productions to camlp4 actions *)
 
 (** This is the part specific to Coq-level Notation and Tactic Notation.
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 2af4ed533..abb463f82 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -8,7 +8,6 @@
 
 open Names
 open Libnames
-open Tok (* necessary for camlp4 *)
 
 open Pcoq
 open Pcoq.Prim
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 7ca2e4a4f..68b8be6b8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -9,7 +9,6 @@
 open Constrexpr
 open Vernacexpr
 open Misctypes
-open Tok
 
 open Pcoq
 open Pcoq.Prim
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8f6b28f13..085c98e37 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -756,11 +756,6 @@ GEXTEND Gram
                  implicit_status = MaximallyImplicit}) items
     ]
   ];
-  name_or_bang: [
-       [ b = OPT "!"; id = name ->
-       not (Option.is_empty b), id
-    ]
-  ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
     [ name = name -> [(snd name, Vernacexpr.NotImplicit)]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index dad98e2e9..9a4766c0b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open CErrors
 open Util
 open Extend
@@ -171,7 +170,6 @@ module Symbols : sig
   val sopt : G.symbol -> G.symbol
   val snterml : G.internal_entry * string -> G.symbol
   val snterm : G.internal_entry -> G.symbol
-  val snterml_level : G.symbol -> string
 end = struct
 
   let stoken tok =
@@ -199,10 +197,6 @@ end = struct
   let slist1 x = Gramext.Slist1 x
   let sopt x = Gramext.Sopt x
 
-  let snterml_level = function
-  | Gramext.Snterml (_, l) -> l
-  | _ -> failwith "snterml_level"
-
 end
 
 let camlp4_verbosity silent f x =
@@ -211,8 +205,6 @@ let camlp4_verbosity silent f x =
   f x;
   warning_verbose := a
 
-let camlp4_verbose f x = camlp4_verbosity (not !Flags.quiet) f x
-
 (** Grammar extensions *)
 
 (** NB: [extend_statment =