Merge branch 'v8.6'

8 files changed, 44 insertions, 51 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index f19759470..542f8f067 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -479,14 +479,6 @@ let find_keyword loc id s =
   | None -> raise Not_found
   | Some c -> KEYWORD c
 
-let process_sequence loc bp c cs =
-  let rec aux n cs =
-    match Stream.peek cs with
-    | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs
-    | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs)
-  in
-  aux 1 cs
-
 (* Must be a special token *)
 let process_chars loc bp c cs =
   let t = progress_from_byte loc None (-1) !token_tree cs c in
@@ -552,12 +544,6 @@ let rec next_token loc = parser bp
       | _ -> ()
       in
       (t, set_loc_pos loc bp ep)
-  | [< ' ('-'|'+'|'*' as c); s >] ->
-      let t,new_between_com =
-        if !between_com then process_sequence loc bp c s, true
-        else process_chars loc bp c s,false
-      in
-      comment_stop bp; between_com := new_between_com; t
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark loc bp s in
       comment_stop bp; (t, set_loc_pos loc ep bp)
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 389c34fa5..a3d0e7133 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -259,7 +259,6 @@ IFDEF CAMLP5 THEN
     | Tok.INT s -> "INT", s
     | Tok.STRING s -> "STRING", s
     | Tok.LEFTQMARK -> "LEFTQMARK", ""
-    | Tok.BULLET s -> "BULLET", s
     | Tok.EOI -> "EOI", ""
     in
     Gramext.Stoken pattern
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ccc7c55a8..47455f984 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -127,7 +127,7 @@ let name_colon =
 let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
 
 GEXTEND Gram
-  GLOBAL: binder_constr lconstr constr operconstr sort global
+  GLOBAL: binder_constr lconstr constr operconstr universe_level sort global
   constr_pattern lconstr_pattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
   record_declaration typeclass_constraint pattern appl_arg;
@@ -295,10 +295,10 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   instance:
-    [ [ "@{"; l = LIST1 level; "}" -> Some l
+    [ [ "@{"; l = LIST1 universe_level; "}" -> Some l
       | -> None ] ]
   ;
-  level:
+  universe_level:
     [ [ "Set" -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 51c4733aa..0b9d4622a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -33,8 +33,6 @@ let _ = List.iter CLexer.add_keyword vernac_kw
 
 let query_command = Gram.entry_create "vernac:query_command"
 
-let subprf = Gram.entry_create "vernac:subprf"
-
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
 let thm_token = Gram.entry_create "vernac:thm_token"
 let def_body = Gram.entry_create "vernac:def_body"
@@ -45,13 +43,25 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
 let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
-let make_bullet s =
-  let n = String.length s in
-  match s.[0] with
-  | '-' -> Dash n
-  | '+' -> Plus n
-  | '*' -> Star n
-  | _ -> assert false
+let subprf = Gram.Entry.of_parser "vernac:subprf" (fun strm ->
+  match get_tok (Stream.peek strm) with
+  | Some (KEYWORD "{") -> Stream.junk strm; VernacSubproof None
+  | Some (KEYWORD "}") -> Stream.junk strm; VernacEndSubproof
+  | Some (KEYWORD k) ->
+    (match k.[0] with
+    | ('-'|'+'|'*') as c ->
+      let n = String.length k in
+      for i = 1 to n - 1 do
+        if k.[i] != c then raise Stream.Failure
+      done;
+      Stream.junk strm;
+      VernacBullet (match c with
+        | '-' -> Dash n
+        | '+' -> Plus n
+        | '*' -> Star n
+        | _ -> assert false)
+    | _ -> raise Stream.Failure)
+  | _ -> raise Stream.Failure)
 
 GEXTEND Gram
   GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
@@ -102,13 +112,6 @@ GEXTEND Gram
     [ [ c = subgoal_command -> c None] ]
   ;
 
-  subprf:
-  [ [ s = BULLET -> VernacBullet (make_bullet s)
-    | "{" -> VernacSubproof None
-    | "}" -> VernacEndSubproof
-    ] ]
-  ;
-
   subgoal_command:
     [ [ c = query_command; "." ->
                   begin function
@@ -226,8 +229,8 @@ GEXTEND Gram
     [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
   ;
   univ_constraint:
-    [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
-	r = identref -> (l, ord, r) ] ]
+    [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
+	r = universe_level -> (l, ord, r) ] ]
   ;
   finite_token:
     [ [ "Inductive" -> (Inductive_kw,Finite)
@@ -653,23 +656,35 @@ GEXTEND Gram
       | IDENT "Arguments"; qid = smart_global; 
         impl = LIST1 [ l = LIST0
         [ item = argument_spec ->
-            let id, r, s = item in [`Id (id,r,s,false,false)]
+            let name, recarg_like, notation_scope = item in
+            [`Id { name=name; recarg_like=recarg_like;
+                   notation_scope=notation_scope;
+                   implicit_status = `NotImplicit}]
         | "/" -> [`Slash]
         | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
             let f x = match sc, x with
             | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
             | Some _, Some _ -> error "scope declared twice" in
-            List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items
+            List.map (fun (name,recarg_like,notation_scope) ->
+              `Id { name=name; recarg_like=recarg_like;
+                    notation_scope=f notation_scope;
+                    implicit_status = `NotImplicit}) items
         | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
             let f x = match sc, x with
             | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
             | Some _, Some _ -> error "scope declared twice" in
-            List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items
+            List.map (fun (name,recarg_like,notation_scope) ->
+              `Id { name=name; recarg_like=recarg_like;
+                    notation_scope=f notation_scope;
+                    implicit_status = `Implicit}) items
         | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
             let f x = match sc, x with
             | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
             | Some _, Some _ -> error "scope declared twice" in
-            List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items
+            List.map (fun (name,recarg_like,notation_scope) ->
+              `Id { name=name; recarg_like=recarg_like;
+                    notation_scope=f notation_scope;
+                    implicit_status = `MaximallyImplicit}) items
         ] -> l ] SEP ",";
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
          let mods = match mods with None -> [] | Some l -> List.flatten l in
@@ -1103,10 +1118,9 @@ GEXTEND Gram
       | IDENT "right"; IDENT "associativity" -> SetAssoc RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc NonA
       | IDENT "only"; IDENT "printing" -> SetOnlyPrinting
-      | IDENT "only"; IDENT "parsing" ->
-        SetOnlyParsing Flags.Current
+      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
       | IDENT "compat"; s = STRING ->
-        SetOnlyParsing (Coqinit.get_compat_version s)
+        SetCompatVersion (Coqinit.get_compat_version s)
       | IDENT "format"; s1 = [s = STRING -> (!@loc,s)];
                         s2 = OPT [s = STRING -> (!@loc,s)] ->
           begin match s1, s2 with
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index ef707790c..9787af826 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -304,6 +304,7 @@ module Constr =
     let binder_constr = gec_constr "binder_constr"
     let ident = make_gen_entry uconstr "ident"
     let global = make_gen_entry uconstr "global"
+    let universe_level = make_gen_entry uconstr "universe_level"
     let sort = make_gen_entry uconstr "sort"
     let pattern = Gram.entry_create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 82ec49417..55868900a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -156,6 +156,7 @@ module Constr :
     val operconstr : constr_expr Gram.entry
     val ident : Id.t Gram.entry
     val global : reference Gram.entry
+    val universe_level : glob_level Gram.entry
     val sort : glob_sort Gram.entry
     val pattern : cases_pattern_expr Gram.entry
     val constr_pattern : constr_expr Gram.entry
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 8ae106512..99d5c972c 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -18,7 +18,6 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
-  | BULLET of string
   | EOI
 
 let equal t1 t2 = match t1, t2 with
@@ -30,7 +29,6 @@ let equal t1 t2 = match t1, t2 with
 | INT s1, INT s2 -> string_equal s1 s2
 | STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
-| BULLET s1, BULLET s2 -> string_equal s1 s2
 | EOI, EOI -> true
 | _ -> false
 
@@ -42,7 +40,6 @@ let extract_string = function
   | FIELD s -> s
   | INT s -> s
   | LEFTQMARK -> "?"
-  | BULLET s -> s
   | EOI -> ""
 
 let to_string = function
@@ -53,7 +50,6 @@ let to_string = function
   | INT s -> Format.sprintf "INT %s" s
   | STRING s -> Format.sprintf "STRING %S" s
   | LEFTQMARK -> "LEFTQMARK"
-  | BULLET s -> Format.sprintf "STRING %S" s
   | EOI -> "EOI"
 
 let match_keyword kwd = function
@@ -75,7 +71,6 @@ let of_pattern = function
   | "INT", s -> INT s
   | "STRING", s -> STRING s
   | "LEFTQMARK", _ -> LEFTQMARK
-  | "BULLET", s -> BULLET s
   | "EOI", _ -> EOI
   | _ -> failwith "Tok.of_pattern: not a constructor"
 
@@ -87,7 +82,6 @@ let to_pattern = function
   | INT s -> "INT", s
   | STRING s -> "STRING", s
   | LEFTQMARK -> "LEFTQMARK", ""
-  | BULLET s -> "BULLET", s
   | EOI -> "EOI", ""
 
 let match_pattern =
@@ -100,7 +94,6 @@ let match_pattern =
     | "INT", "" -> (function INT s -> s | _ -> err ())
     | "STRING", "" -> (function STRING s -> s | _ -> err ())
     | "LEFTQMARK", "" -> (function LEFTQMARK -> ""  | _ -> err ())
-    | "BULLET", "" ->  (function BULLET s -> s  | _ -> err ())
     | "EOI", "" -> (function EOI -> "" | _ -> err ())
     | pat ->
 	let tok = of_pattern pat in
diff --git a/parsing/tok.mli b/parsing/tok.mli
index b9286c53e..b1e79dc90 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -16,7 +16,6 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
-  | BULLET of string
   | EOI
 
 val equal : t -> t -> bool