Merge branch 'master'.

5 files changed, 43 insertions, 47 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 69e4eb8d27..02a720d2d9 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -408,24 +408,6 @@ let comment_stop ep =
   comment_begin := None;
   between_commands := false
 
-(* Does not unescape!!! *)
-let rec comm_string loc bp = parser
-  | [< ''"' >] -> push_string "\""; loc
-  | [< ''\\'; loc =
-           (parser [< ' ('"' | '\\' as c) >] ->
-              let () = match c with
-              | '"' -> real_push_char c
-              | _ -> ()
-              in
-              real_push_char c; loc
-                 | [< >] -> real_push_char '\\'; loc); s >]
-     -> comm_string loc bp s
-  | [< _ = Stream.empty >] ep ->
-      let loc = set_loc_pos loc bp ep in
-      err loc Unterminated_string
-  | [< ''\n' as c; s >] ep -> real_push_char c; comm_string (bump_loc_line loc ep) bp s
-  | [< 'c; s >] -> real_push_char c; comm_string loc bp s
-
 let rec comment loc bp = parser bp2
   | [< ''(';
        loc = (parser
@@ -437,12 +419,8 @@ let rec comment loc bp = parser bp2
          | [< '')' >] -> push_string "*)"; loc
          | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc
   | [< ''"'; s >] ->
-      let loc =
-	(* In beautify mode, the lexing differs between strings in comments and
-	   regular strings (e.g. escaping). It seems wrong. *)
-	if !Flags.beautify then (push_string"\""; comm_string loc bp2 s)
-	else fst (string loc ~comm_level:(Some 0) bp2 0 s)
-      in
+      let loc, len = string loc ~comm_level:(Some 0) bp2 0 s in
+      push_string "\""; push_string (get_buff len); push_string "\"";
       comment loc bp s
   | [< _ = Stream.empty >] ep ->
       let loc = set_loc_pos loc bp ep in
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 2adbf300e9..4c52805381 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -98,10 +98,9 @@ GEXTEND Gram
       (* Declare "Resolve" explicitly so as to be able to later extend with
          "Resolve ->" and "Resolve <-" *)
       | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; 
-	  pri = OPT [ "|"; i = natural -> i ];
-	  dbnames = opt_hintbases ->
+	info = hint_info; dbnames = opt_hintbases ->
 	  VernacHints (false,dbnames,
-	    HintsResolve (List.map (fun x -> (pri, true, x)) lc))
+	    HintsResolve (List.map (fun x -> (info, true, x)) lc))
       ] ];
   obsolete_locality:
     [ [ IDENT "Local" -> true | -> false ] ]
@@ -111,9 +110,8 @@ GEXTEND Gram
      | c = constr -> HintsConstr c ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; 
-	pri = OPT [ "|"; i = natural -> i ] ->
-          HintsResolve (List.map (fun x -> (pri, true, x)) lc)
+    [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
+          HintsResolve (List.map (fun x -> (info, true, x)) lc)
       | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
       | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
       | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7bc5bfca38..d46880831f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -582,7 +582,7 @@ let warn_deprecated_implicit_arguments =
 
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
-  GLOBAL: gallina_ext instance_name;
+  GLOBAL: gallina_ext instance_name hint_info;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -635,17 +635,20 @@ GEXTEND Gram
 
       | IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
-	 pri = OPT [ "|"; i = natural -> i ] ;
+	 info = hint_info ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) |
 	     ":="; c = lconstr -> Some (false,c) | -> None ] ->
-	   VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri)
+	   VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info)
 
       | IDENT "Existing"; IDENT "Instance"; id = global;
-          pri = OPT [ "|"; i = natural -> i ] ->
-	  VernacDeclareInstances ([id], pri)
+          info = hint_info ->
+	  VernacDeclareInstances [id, info]
+
       | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
-          pri = OPT [ "|"; i = natural -> i ] ->
-	  VernacDeclareInstances (ids, pri)
+        pri = OPT [ "|"; i = natural -> i ] ->
+         let info = { hint_priority = pri; hint_pattern = None } in
+         let insts = List.map (fun i -> (i, info)) ids in
+	  VernacDeclareInstances insts
 
       | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
 
@@ -764,6 +767,11 @@ 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)]
@@ -786,6 +794,11 @@ GEXTEND Gram
           (Option.default [] sup)
       | -> ((!@loc, Anonymous), None), []  ] ]
   ;
+  hint_info:
+    [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
+         { hint_priority = i; hint_pattern = pat }
+      | -> { hint_priority = None; hint_pattern = None } ] ]
+  ;
   reserv_list:
     [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
   ;
@@ -807,8 +820,8 @@ GEXTEND Gram
       (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
       | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
-	 pri = OPT [ "|"; i = natural -> i ] ->
-	   VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri)
+	 info = hint_info ->
+	   VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info)
 
       (* System directory *)
       | IDENT "Pwd" -> VernacChdir None
@@ -866,11 +879,16 @@ GEXTEND Gram
       | "Set"; table = option_table; v = option_value ->
         begin match v with
         | StringValue s ->
-          let (last, prefix) = List.sep_last table in
-          if String.equal last "Append" && not (List.is_empty prefix) then
-            VernacSetAppendOption (prefix, s)
+          (* We make a special case for warnings because appending is their
+          natural semantics *)
+          if CString.List.equal table ["Warnings"] then
+            VernacSetAppendOption (table, s)
           else
-            VernacSetOption (table, v)
+            let (last, prefix) = List.sep_last table in
+            if String.equal last "Append" && not (List.is_empty prefix) then
+              VernacSetAppendOption (prefix, s)
+            else
+              VernacSetOption (table, v)
         | _ -> VernacSetOption (table, v)
         end
       | "Set"; table = option_table ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9787af8264..c5823440ac 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -338,6 +338,7 @@ module Vernac_ =
     let vernac_eoi = eoi_entry vernac
     let rec_definition = gec_vernac "Vernac.rec_definition"
     let red_expr = make_gen_entry utactic "red_expr"
+    let hint_info = gec_vernac "hint_info"
     (* Main vernac entry *)
     let main_entry = Gram.entry_create "vernac"
     let noedit_mode = gec_vernac "noedit_command"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 55868900a9..d987bb4557 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -38,7 +38,7 @@ module Gram : module type of Compat.GrammarMake(CLexer)
         |     (together with a constr entry level, e.g. 50, and indications of)
         |     (subentries, e.g. x in constr next level and y constr same level)
         |
-        | spliting into tokens by Metasyntax.split_notation_string
+        | splitting into tokens by Metasyntax.split_notation_string
         V
       [String "x"; String "+"; String "y"] : symbol_token list
         |
@@ -95,7 +95,7 @@ module Gram : module type of Compat.GrammarMake(CLexer)
 
 *)
 
-(** Temporary activate camlp4 verbosity *)
+(** Temporarily activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
@@ -189,6 +189,7 @@ module Vernac_ :
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
     val red_expr : raw_red_expr Gram.entry
+    val hint_info : Vernacexpr.hint_info_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
@@ -207,14 +208,14 @@ type gram_reinit = gram_assoc * gram_position
 
 val grammar_extend : 'a Gram.entry -> gram_reinit option ->
   'a Extend.extend_statment -> unit
-(** Extend the grammar of Coq, without synchronizing it with the bactracking
+(** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
 
 (** {5 Extending the parser with summary-synchronized commands} *)
 
 module GramState : Store.S
-(** Auxilliary state of the grammar. Any added data must be marshallable. *)
+(** Auxiliary state of the grammar. Any added data must be marshallable. *)
 
 type 'a grammar_command
 (** Type of synchronized parsing extensions. The ['a] type should be