Merge branch 'trunk' into located_switch

10 files changed, 21 insertions, 63 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 712d10a96..6940fd6fb 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/egramml.ml b/parsing/egramml.ml
index 1c6346a8f..07c77619f 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -17,7 +17,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      ('a raw_abstract_argument_type * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
+      ('a raw_abstract_argument_type option * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
@@ -38,7 +38,7 @@ let rec ty_rule_of_gram = function
   AnyTyRule r
 | GramNonTerminal (_, (t, tok)) :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let inj = Some (fun obj -> Genarg.in_gen t obj) in
+  let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 1a3ae173c..030d39605 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -15,7 +15,7 @@ open Vernacexpr
 
 type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
+  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option *
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index a44aa5400..54bac253d 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -146,12 +146,12 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType []
-      | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
+      | "Type"; "@{"; u = universe; "}" -> GType u
       ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
-      | id = identref -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
+      | id = name -> [id]
       ] ]
   ;
   lconstr:
@@ -302,7 +302,7 @@ GEXTEND Gram
     [ [ "Set" -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
+      | id = name -> GType (Some id)
       ] ]
   ;
   fix_constr:
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index d94c5e963..78f75a73c 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 ee0f06fe0..a3f9793bb 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
@@ -49,14 +48,11 @@ GEXTEND Gram
       | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
           VernacEndProof (Proved (Opaque (Some l),None))
-      | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None))
-      | IDENT "Save"; tok = thm_token; id = identref ->
-	  VernacEndProof (Proved (Opaque None,Some (id,Some tok)))
       | IDENT "Save"; id = identref ->
-	  VernacEndProof (Proved (Opaque None,Some (id,None)))
+	  VernacEndProof (Proved (Opaque None, Some id))
       | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
       |	IDENT "Defined"; id=identref ->
-	  VernacEndProof (Proved (Transparent,Some (id,None)))
+	  VernacEndProof (Proved (Transparent,Some id))
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7239bc23b..b5d0780bd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -136,8 +136,8 @@ GEXTEND Gram
     [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
         l = LIST0
           [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
-          (Some id,(bl,c,None)) ] ->
-          VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
+          (Some id,(bl,c)) ] ->
+          VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
@@ -757,11 +757,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 =