Imported Upstream version 8.6upstream/8.6

20 files changed, 1801 insertions, 2251 deletions

diff --git a/parsing/lexer.ml4 b/parsing/cLexer.ml4
index 5d96873f..aec6a326 100644
--- a/parsing/lexer.ml4
+++ b/parsing/cLexer.ml4
@@ -8,8 +8,8 @@
 
 open Pp
 open Util
-open Compat
 open Tok
+open Compat
 
 (* Dictionaries: trees annotated with string options, each node being a map
    from chars to dictionaries (the subtrees). A trie, in other words. *)
@@ -69,6 +69,15 @@ let ttree_remove ttree str =
   in
   remove ttree 0
 
+let ttree_elements ttree =
+  let rec elts tt accu =
+    let accu = match tt.node with
+    | None -> accu
+    | Some s -> CString.Set.add s accu
+    in
+    CharMap.fold (fun _ tt accu -> elts tt accu) tt.branch accu
+  in
+  elts ttree CString.Set.empty
 
 (* Errors occurring while lexing (explained as "Lexer error: ...") *)
 
@@ -96,12 +105,12 @@ module Error = struct
              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))
+  let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x))
 
 end
 open Error
 
-let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str)
+let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
@@ -112,64 +121,61 @@ type token_kind =
   | AsciiChar
   | EmptyStream
 
-let error_unsupported_unicode_character n unicode cs =
-  let bp = Stream.count cs in
-  err (bp,bp+n) (UnsupportedUnicode unicode)
-
-let error_utf8 cs =
+let error_utf8 loc cs =
   let bp = Stream.count cs in
   Stream.junk cs; (* consume the char to avoid read it and fail again *)
-  err (bp, bp+1) Illegal_character
+  let loc = set_loc_pos loc bp (bp+1) in
+  err loc Illegal_character
 
-let utf8_char_size cs = function
+let utf8_char_size loc cs = function
   (* Utf8 leading byte *)
   | '\x00'..'\x7F' -> 1
   | '\xC0'..'\xDF' -> 2
   | '\xE0'..'\xEF' -> 3
   | '\xF0'..'\xF7' -> 4
-  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs
+  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 loc cs
 
 let njunk n = Util.repeat n Stream.junk
 
-let check_utf8_trailing_byte cs c =
-  if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 cs
+let check_utf8_trailing_byte loc cs c =
+  if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 loc cs
 
 (* Recognize utf8 blocks (of length less than 4 bytes) *)
 (* but don't certify full utf8 compliance (e.g. no emptyness check) *)
-let lookup_utf8_tail c cs =
+let lookup_utf8_tail loc c cs =
   let c1 = Char.code c in
-  if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 cs
+  if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 loc cs
   else
     let n, unicode =
       if Int.equal (c1 land 0x20) 0 then
       match Stream.npeek 2 cs with
       | [_;c2] ->
-          check_utf8_trailing_byte cs c2;
+          check_utf8_trailing_byte loc cs c2;
           2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F)
-      | _ -> error_utf8 cs
+      | _ -> error_utf8 loc cs
       else if Int.equal (c1 land 0x10) 0 then
       match Stream.npeek 3 cs with
       | [_;c2;c3] ->
-          check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3;
+          check_utf8_trailing_byte loc cs c2;
+	  check_utf8_trailing_byte loc cs c3;
           3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 +
           (Char.code c3 land 0x3F)
-      | _ -> error_utf8 cs
+      | _ -> error_utf8 loc cs
       else match Stream.npeek 4 cs with
       | [_;c2;c3;c4] ->
-          check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3;
-          check_utf8_trailing_byte cs c4;
+          check_utf8_trailing_byte loc cs c2;
+	  check_utf8_trailing_byte loc cs c3;
+          check_utf8_trailing_byte loc cs c4;
           4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 +
           (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F)
-      | _ -> error_utf8 cs
+      | _ -> error_utf8 loc cs
     in
-    try Unicode.classify unicode, n
-    with Unicode.Unsupported ->
-      njunk n cs; error_unsupported_unicode_character n unicode cs
+    Utf8Token (Unicode.classify unicode, n)
 
-let lookup_utf8 cs =
+let lookup_utf8 loc cs =
   match Stream.peek cs with
     | Some ('\x00'..'\x7F') -> AsciiChar
-    | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs)
+    | Some ('\x80'..'\xFF' as c) -> lookup_utf8_tail loc c cs
     | None -> EmptyStream
 
 let unlocated f x = f x
@@ -180,20 +186,13 @@ let check_keyword str =
   let rec loop_symb = parser
     | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str
     | [< s >] ->
-        match unlocated lookup_utf8 s with
+        match unlocated lookup_utf8 Compat.CompatLoc.ghost s with
         | Utf8Token (_,n) -> njunk n s; loop_symb s
         | AsciiChar -> Stream.junk s; loop_symb s
         | EmptyStream -> ()
   in
   loop_symb (Stream.of_string str)
 
-let check_keyword_to_add s =
-  try check_keyword s
-  with Error.E (UnsupportedUnicode unicode) ->
-    Flags.if_verbose msg_warning
-      (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
-                               which will not be parsable." s unicode))
-
 let check_ident str =
   let rec loop_id intail = parser
     | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] ->
@@ -201,7 +200,7 @@ let check_ident str =
     | [< ' ('0'..'9' | ''') when intail; s >] ->
         loop_id true s
     | [< s >] ->
-        match unlocated lookup_utf8 s with
+        match unlocated lookup_utf8 Compat.CompatLoc.ghost s with
         | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s
         | Utf8Token (Unicode.IdentPart, n) when intail ->
           njunk n s;
@@ -224,13 +223,15 @@ let is_keyword s =
 let add_keyword str =
   if not (is_keyword str) then
     begin
-      check_keyword_to_add str;
+      check_keyword str;
       token_tree := ttree_add !token_tree str
     end
 
 let remove_keyword str =
   token_tree := ttree_remove !token_tree str
 
+let keywords () = ttree_elements !token_tree
+
 (* Freeze and unfreeze the state of the lexer *)
 type frozen_t = ttree
 
@@ -254,87 +255,133 @@ let get_buff len = String.sub !buff 0 len
 
 (* The classical lexer: idents, numbers, quoted strings, comments *)
 
-let rec ident_tail len = parser
+let warn_unrecognized_unicode =
+  CWarnings.create ~name:"unrecognized-unicode" ~category:"parsing"
+         (fun (u,id) ->
+          strbrk (Printf.sprintf "Not considering unicode character \"%s\" of unknown \
+                                  lexical status as part of identifier \"%s\"." u id))
+
+let rec ident_tail loc len = parser
   | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] ->
-      ident_tail (store len c) s
+      ident_tail loc (store len c) s
   | [< s >] ->
-      match lookup_utf8 s with
+      match lookup_utf8 loc s with
       | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) ->
-          ident_tail (nstore n len s) s
+          ident_tail loc (nstore n len s) s
+      | Utf8Token (Unicode.Unknown, n) ->
+          let id = get_buff len in
+          let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in
+          warn_unrecognized_unicode ~loc:!@loc (u,id); len
       | _ -> len
 
 let rec number len = parser
   | [< ' ('0'..'9' as c); s >] -> number (store len c) s
   | [< >] -> len
 
-let rec string in_comments bp len = parser
+let warn_comment_terminator_in_string =
+  CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing"
+         (fun () ->
+          (strbrk
+             "Not interpreting \"*)\" as the end of current \
+              non-terminated comment because it occurs in a \
+              non-terminated string of the comment."))
+
+(* If the string being lexed is in a comment, [comm_level] is Some i with i the
+   current level of comments nesting. Otherwise, [comm_level] is None. *)
+let rec string loc ~comm_level bp len = parser
   | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
-      if esc then string in_comments bp (store len '"') s else len
+      if esc then string loc ~comm_level bp (store len '"') s else (loc, len)
   | [< ''('; s >] ->
       (parser
         | [< ''*'; s >] ->
-            string
-              (Option.map succ in_comments)
+            string loc
+              (Option.map succ comm_level)
               bp (store (store len '(') '*')
               s
         | [< >] ->
-            string in_comments bp (store len '(') s) s
+            string loc comm_level bp (store len '(') s) s
   | [< ''*'; s >] ->
       (parser
         | [< '')'; s >] ->
-            let () = match in_comments with
+            let () = match comm_level with
             | Some 0 ->
-                msg_warning
-                  (strbrk
-                     "Not interpreting \"*)\" as the end of current \
-                      non-terminated comment because it occurs in a \
-                      non-terminated string of the comment.")
+	       warn_comment_terminator_in_string ~loc:!@loc ()
             | _ -> ()
             in
-            let in_comments = Option.map pred in_comments in
-            string in_comments bp (store (store len '*') ')') s
+            let comm_level = Option.map pred comm_level in
+            string loc comm_level bp (store (store len '*') ')') s
         | [< >] ->
-            string in_comments bp (store len '*') s) s
-  | [< 'c; s >] -> string in_comments bp (store len c) s
-  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
+            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
+     line. *)
+     let loc =
+       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
+  | [< _ = Stream.empty >] ep ->
+     let loc = set_loc_pos loc bp ep in
+     err loc Unterminated_string
 
 (* Hook for exporting comment into xml theory files *)
 let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
 
+(* To associate locations to a file name *)
+let current_file = ref None
+
 (* Utilities for comments in beautify *)
 let comment_begin = ref None
 let comm_loc bp = match !comment_begin with
 | None -> comment_begin := Some bp
 | _ -> ()
 
-let current = Buffer.create 8192
-let between_com = ref true
+let comments = ref []
+let current_comment = Buffer.create 8192
+let between_commands = ref true
 
-type com_state = int option * string * bool
-let restore_com_state (o,s,b) =
+let rec split_comments comacc acc pos = function
+    [] -> comments := List.rev acc; comacc
+  | ((b,e),c as com)::coms ->
+      (* Take all comments that terminates before pos, or begin exactly
+         at pos (used to print comments attached after an expression) *)
+      if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
+      else split_comments comacc (com::acc) pos coms
+
+let extract_comments pos = split_comments [] [] pos !comments
+
+(* The state of the lexer visible from outside *)
+type lexer_state = int option * string * bool * ((int * int) * string) list * string option
+
+let init_lexer_state f = (None,"",true,[],f)
+let set_lexer_state (o,s,b,c,f) =
   comment_begin := o;
-  Buffer.clear current; Buffer.add_string current s;
-  between_com := b
-let dflt_com = (None,"",true)
-let com_state () =
-  let s = (!comment_begin, Buffer.contents current, !between_com) in
-  restore_com_state dflt_com; s
+  Buffer.clear current_comment; Buffer.add_string current_comment s;
+  between_commands := b;
+  comments := c;
+  current_file := f
+let release_lexer_state () =
+  (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
+let drop_lexer_state () =
+    set_lexer_state (init_lexer_state None)
 
-let real_push_char c = Buffer.add_char current c
+let real_push_char c = Buffer.add_char current_comment c
 
 (* Add a char if it is between two commands, if it is a newline or
    if the last char is not a space itself. *)
 let push_char c =
   if
-    !between_com || List.mem c ['\n';'\r'] ||
+    !between_commands || List.mem c ['\n';'\r'] ||
     (List.mem c [' ';'\t']&&
-     (Int.equal (Buffer.length current) 0 ||
-      not (let s = Buffer.contents current in
+     (Int.equal (Buffer.length current_comment) 0 ||
+      not (let s = Buffer.contents current_comment in
            List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r'])))
   then
     real_push_char c
 
-let push_string s = Buffer.add_string current s
+let push_string s = Buffer.add_string current_comment s
 
 let null_comment s =
   let rec null i =
@@ -342,146 +389,134 @@ let null_comment s =
   null (String.length s - 1)
 
 let comment_stop ep =
-  let current_s = Buffer.contents current in
-  if !Flags.xml_export && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  let current_s = Buffer.contents current_comment in
+  if !Flags.xml_export && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
       Hook.get f_xml_output_comment current_s;
-  (if Flags.do_beautify() && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  (if !Flags.beautify && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
-          msgerrnl(str "No begin location for comment '"
-                   ++ str current_s ++str"' ending at  "
-                   ++ int ep);
+          Feedback.msg_notice
+            (str "No begin location for comment '"
+             ++ str current_s ++str"' ending at  "
+             ++ int ep);
           ep-1 in
-    Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
-  Buffer.clear current;
+    comments := ((bp,ep),current_s) :: !comments);
+  Buffer.clear current_comment;
   comment_begin := None;
-  between_com := false
-
-(* Does not unescape!!! *)
-let rec comm_string bp = parser
-  | [< ''"' >] -> push_string "\""
-  | [< ''\\'; _ =
-           (parser [< ' ('"' | '\\' as c) >] ->
-              let () = match c with
-              | '"' -> real_push_char c
-              | _ -> ()
-              in
-              real_push_char c
-                 | [< >] -> real_push_char '\\'); s >]
-     -> comm_string bp s
-  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
-  | [< 'c; s >] -> real_push_char c; comm_string bp s
-
-let rec comment bp = parser bp2
+  between_commands := false
+
+let rec comment loc bp = parser bp2
   | [< ''(';
-       _ = (parser
-              | [< ''*'; s >] -> push_string "(*"; comment bp s
-              | [< >] -> push_string "(" );
-       s >] -> comment bp s
+       loc = (parser
+              | [< ''*'; s >] -> push_string "(*"; comment loc bp s
+              | [< >] -> push_string "("; loc );
+       s >] -> comment loc bp s
   | [< ''*';
-       _ = parser
-         | [< '')' >] -> push_string "*)";
-         | [< s >] -> real_push_char '*'; comment bp s >] -> ()
+       loc = parser
+         | [< '')' >] -> push_string "*)"; loc
+         | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc
   | [< ''"'; s >] ->
-      if Flags.do_beautify() then (push_string"\"";comm_string bp2 s)
-      else ignore (string (Some 0) bp2 0 s);
-      comment bp s
-  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
-  | [< 'z; s >] -> real_push_char z; comment bp s
+      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
+      err loc Unterminated_comment
+  | [< ''\n' as z; s >] ep -> real_push_char z; comment (bump_loc_line loc ep) bp s
+  | [< 'z; s >] -> real_push_char z; comment loc bp s
 
 (* Parse a special token, using the [token_tree] *)
 
 (* Peek as much utf-8 lexemes as possible *)
 (* and retain the longest valid special token obtained *)
-let rec progress_further last nj tt cs =
-  try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
+let rec progress_further loc last nj tt cs =
+  try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
   with Failure _ -> last
 
-and update_longest_valid_token last nj tt cs =
+and update_longest_valid_token loc last nj tt cs =
   match tt.node with
   | Some _ as last' ->
     stream_njunk nj cs;
-    progress_further last' 0 tt cs
+    progress_further loc last' 0 tt cs
   | None ->
-    progress_further last nj tt cs
+    progress_further loc last nj tt cs
 
 (* nj is the number of char peeked since last valid token *)
 (* n the number of char in utf8 block *)
-and progress_utf8 last nj n c tt cs =
+and progress_utf8 loc last nj n c tt cs =
   try
     let tt = CharMap.find c tt.branch in
     if Int.equal n 1 then
-      update_longest_valid_token last (nj+n) tt cs
+      update_longest_valid_token loc last (nj+n) tt cs
     else
       match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with
       | l when Int.equal (List.length l) (n - 1) ->
-         List.iter (check_utf8_trailing_byte cs) l;
+         List.iter (check_utf8_trailing_byte loc cs) l;
          let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in
-         update_longest_valid_token last (nj+n) tt cs
+         update_longest_valid_token loc last (nj+n) tt cs
       | _ ->
-          error_utf8 cs
+          error_utf8 loc cs
   with Not_found ->
     last
 
-and progress_from_byte last nj tt cs c =
-  progress_utf8 last nj (utf8_char_size cs c) c tt cs
+and progress_from_byte loc last nj tt cs c =
+  progress_utf8 loc last nj (utf8_char_size loc cs c) c tt cs
 
-let find_keyword id s =
+let find_keyword loc id s =
   let tt = ttree_find !token_tree id in
-  match progress_further tt.node 0 tt s with
+  match progress_further loc tt.node 0 tt s with
   | None -> raise Not_found
   | Some c -> KEYWORD c
 
-let process_sequence bp c cs =
+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), (bp, Stream.count 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 bp c cs =
-  let t = progress_from_byte None (-1) !token_tree cs c in
+let process_chars loc bp c cs =
+  let t = progress_from_byte loc None (-1) !token_tree cs c in
   let ep = Stream.count cs in
   match t with
-    | Some t -> (KEYWORD t, (bp, ep))
+    | Some t -> (KEYWORD t, set_loc_pos loc bp ep)
     | None ->
-        let ep' = bp + utf8_char_size cs c in
+        let ep' = bp + utf8_char_size loc cs c in
         njunk (ep' - ep) cs;
-        err (bp, ep') Undefined_token
-
-let token_of_special c s = match c with
-  | '$' -> METAIDENT s
-  | '.' -> FIELD s
-  | _ -> assert false
+	let loc = set_loc_pos loc bp ep' in
+        err loc Undefined_token
 
-(* Parse what follows a dot / a dollar *)
+(* Parse what follows a dot *)
 
-let parse_after_special c bp =
+let parse_after_dot loc c bp =
   parser
-  | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail (store 0 d) >] ->
-      token_of_special c (get_buff len)
+  | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d); s >] ->
+      let field = get_buff len in
+      (try find_keyword loc ("."^field) s with Not_found -> FIELD field)
   | [< s >] ->
-      match lookup_utf8 s with
+      match lookup_utf8 loc s with
       | Utf8Token (Unicode.Letter, n) ->
-          token_of_special c (get_buff (ident_tail (nstore n 0 s) s))
-      | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s)
+          let len = ident_tail loc (nstore n 0 s) s in
+          let field = get_buff len in
+          (try find_keyword loc ("."^field) s with Not_found -> FIELD field)
+      | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s)
 
 (* Parse what follows a question mark *)
 
-let parse_after_qmark bp s =
+let parse_after_qmark loc bp s =
   match Stream.peek s with
     | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK
     | None -> KEYWORD "?"
     | _ ->
-        match lookup_utf8 s with
+        match lookup_utf8 loc s with
           | Utf8Token (Unicode.Letter, _) -> LEFTQMARK
           | AsciiChar | Utf8Token _ | EmptyStream ->
-            fst (process_chars bp '?' s)
+            fst (process_chars loc bp '?' s)
 
 let blank_or_eof cs =
   match Stream.peek cs with
@@ -491,71 +526,76 @@ let blank_or_eof cs =
 
 (* Parse a token in a char stream *)
 
-let rec next_token = parser bp
-  | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
-      comm_loc bp; push_char c; next_token s
-  | [< ''$' as c; t = parse_after_special c bp >] ep ->
-      comment_stop bp; (t, (ep, bp))
-  | [< ''.' as c; t = parse_after_special c bp; s >] ep ->
+let rec next_token loc = parser bp
+  | [< ''\n' as c; s >] ep ->
+      comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s
+  | [< '' ' | '\t' | '\r' as c; s >] ->
+      comm_loc bp; push_char c; next_token loc s
+  | [< ''.' as c; t = parse_after_dot loc c bp; s >] ep ->
       comment_stop bp;
       (* We enforce that "." should either be part of a larger keyword,
          for instance ".(", or followed by a blank or eof. *)
       let () = match t with
       | KEYWORD ("." | "...") ->
-        if not (blank_or_eof s) then err (bp,ep+1) Undefined_token;
-        between_com := true;
+        if not (blank_or_eof s) then
+	  err (set_loc_pos loc bp (ep+1)) Undefined_token;
+	between_commands := true;
       | _ -> ()
       in
-      (t, (bp,ep))
+      (t, set_loc_pos loc bp ep)
   | [< ' ('-'|'+'|'*' as c); s >] ->
-      let t,new_between_com =
-        if !between_com then process_sequence bp c s,true
-        else process_chars bp c s,false
+      let t,new_between_commands =
+        if !between_commands 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
+      comment_stop bp; between_commands := new_between_commands; t
   | [< ''?'; s >] ep ->
-      let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
+      let t = parse_after_qmark loc bp s in
+      comment_stop bp; (t, set_loc_pos loc bp ep)
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
-       len = ident_tail (store 0 c); s >] ep ->
+       len = ident_tail loc (store 0 c); s >] ep ->
       let id = get_buff len in
       comment_stop bp;
-      (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
+      (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
       comment_stop bp;
-      (INT (get_buff len), (bp, ep))
-  | [< ''\"'; len = string None bp 0 >] ep ->
+      (INT (get_buff len), set_loc_pos loc bp ep)
+  | [< ''\"'; (loc,len) = string loc None bp 0 >] ep ->
       comment_stop bp;
-      (STRING (get_buff len), (bp, ep))
+      (STRING (get_buff len), set_loc_pos loc bp ep)
   | [< ' ('(' as c);
       t = parser
         | [< ''*'; s >] ->
             comm_loc bp;
             push_string "(*";
-            comment bp s;
-            next_token s
-        | [< t = process_chars bp c >] -> comment_stop bp; t >] ->
+            let loc = comment loc bp s in next_token loc s
+        | [< t = process_chars loc bp c >] -> comment_stop bp; t >] ->
       t
+  | [< ' ('{' | '}' as c); s >] ep ->
+      let t,new_between_commands =
+        if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true
+        else process_chars loc bp c s, false
+      in
+      comment_stop bp; between_commands := new_between_commands; t
   | [< s >] ->
-      match lookup_utf8 s with
+      match lookup_utf8 loc s with
         | Utf8Token (Unicode.Letter, n) ->
-            let len = ident_tail (nstore n 0 s) s in
+            let len = ident_tail loc (nstore n 0 s) s in
             let id = get_buff len in
             let ep = Stream.count s in
             comment_stop bp;
-            (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
-        | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) ->
-            let t = process_chars bp (Stream.next s) s in
-            let new_between_com = match t with
-              (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in
-            comment_stop bp; between_com := new_between_com; t
+            (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
+        | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) ->
+            let t = process_chars loc bp (Stream.next s) s in
+            comment_stop bp; t
         | EmptyStream ->
-            comment_stop bp; (EOI, (bp, bp + 1))
+            comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
 
 (* (* Debug: uncomment this for tracing tokens seen by coq...*)
-let next_token s =
-  let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t);
-  (t,(bp,ep))
-*)
+let next_token loc s =
+  let (t,loc as r) = next_token loc s in
+  Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t);
+  r *)
 
 (* Location table system for creating tables associating a token count
    to its location in a char stream (the source) *)
@@ -569,12 +609,6 @@ let loct_func loct i =
 
 let loct_add loct i loc = Hashtbl.add loct i loc
 
-let current_location_table = ref (loct_create ())
-
-type location_table = (int, CompatLoc.t) Hashtbl.t
-let location_table () = !current_location_table
-let restore_location_table t = current_location_table := t
-
 (** {6 The lexer of Coq} *)
 
 (** Note: removing a token.
@@ -604,13 +638,14 @@ let token_text = function
 
 let func cs =
   let loct = loct_create () in
+  let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
   let ts =
     Stream.from
       (fun i ->
-         let (tok, loc) = next_token cs in
-         loct_add loct i (make_loc loc); Some tok)
+         let (tok, loc) = next_token !cur_loc cs in
+	 cur_loc := Compat.after loc;
+         loct_add loct i loc; Some tok)
   in
-  current_location_table := loct;
   (ts, loct_func loct)
 
 let lexer = {
@@ -628,10 +663,10 @@ ELSE (* official camlp4 for ocaml >= 3.10 *)
 
 module M_ = Camlp4.ErrorHandler.Register (Error)
 
-module Loc = CompatLoc
+module Loc = Compat.CompatLoc
 module Token = struct
   include Tok (* Cf. tok.ml *)
-  module Loc = CompatLoc
+  module Loc = Compat.CompatLoc
   module Error = Camlp4.Struct.EmptyError
   module Filter = struct
     type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t
@@ -644,16 +679,18 @@ module Token = struct
   end
 end
 
-let mk () _init_loc(*FIXME*) cs =
+let mk () =
   let loct = loct_create () in
-  let rec self =
+  let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
+  let rec self init_loc (* FIXME *) =
     parser i
-       [< (tok, loc) = next_token; s >] ->
-          let loc = make_loc loc in
-            loct_add loct i loc;
-            [< '(tok, loc); self s >]
+       [< (tok, loc) = next_token !cur_loc; s >] ->
+            cur_loc := Compat.set_loc_file loc !current_file;
+	    loct_add loct i loc;
+            [< '(tok, loc); self init_loc s >]
       | [< >] -> [< >]
-  in current_location_table := loct; self cs
+  in
+  self
 
 END
 
@@ -689,7 +726,7 @@ let strip s =
 
 let terminal s =
   let s = strip s in
-  let () = match s with "" -> Errors.error "empty token." | _ -> () in
+  let () = match s with "" -> failwith "empty token." | _ -> () in
   if is_ident_not_keyword s then IDENT s
   else if is_number s then INT s
   else KEYWORD s
diff --git a/parsing/lexer.mli b/parsing/cLexer.mli
index 24b0ec84..e0fdf8cb 100644
--- a/parsing/lexer.mli
+++ b/parsing/cLexer.mli
@@ -9,13 +9,7 @@
 val add_keyword : string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
-
-(* val location_function : int -> Loc.t *)
-
-(** for coqdoc *)
-type location_table
-val location_table : unit -> location_table
-val restore_location_table : location_table -> unit
+val keywords : unit -> CString.Set.t
 
 val check_ident : string -> unit
 val is_ident : string -> bool
@@ -25,12 +19,12 @@ type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
 
-type com_state
-val com_state: unit -> com_state
-val restore_com_state: com_state -> unit
-
 val xml_output_comment : (string -> unit) Hook.t
 
+(* Retrieve the comments lexed at a given location of the stream
+   currently being processeed *)
+val extract_comments : int -> string list
+
 val terminal : string -> Tok.t
 
 (** The lexer of Coq: *)
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index d1d55c81..befa0d01 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -10,6 +10,10 @@
 
 (** Locations *)
 
+let file_loc_of_file = function
+| None -> ""
+| Some f -> f
+
 IFDEF CAMLP5 THEN
 
 module CompatLoc = struct
@@ -20,23 +24,49 @@ end
 
 exception Exc_located = Ploc.Exc
 
-IFDEF CAMLP5_6_00 THEN
-let ploc_make_loc fname lnb pos bpep = Ploc.make_loc fname lnb pos bpep ""
-let ploc_file_name = Ploc.file_name
-ELSE
-let ploc_make_loc fname lnb pos bpep = Ploc.make lnb pos bpep
-let ploc_file_name _ = ""
-END
-
-let of_coqloc loc =
-  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
-  ploc_make_loc fname lnb pos (bp,ep)
-
 let to_coqloc loc =
-  Loc.create (ploc_file_name loc) (Ploc.line_nb loc)
-    (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc)
+  { Loc.fname = Ploc.file_name loc;
+    Loc.line_nb = Ploc.line_nb loc;
+    Loc.bol_pos = Ploc.bol_pos loc;
+    Loc.bp = Ploc.first_pos loc;
+    Loc.ep = Ploc.last_pos loc;
+    Loc.line_nb_last = Ploc.line_nb_last loc;
+    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
+
+let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""
+
+(* Update a loc without allocating an intermediate pair *)
+let set_loc_pos loc bp ep =
+  Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp)
+
+(* Increase line number by 1 and update position of beginning of line *)
+let bump_loc_line loc bol_pos =
+  Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos
+		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+
+(* Same as [bump_loc_line], but for the last line in location *)
+(* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop,
+   so we have to resort to a hack merging two locations. *)
+(* Warning: [bump_loc_line_last] changes the end position. You may need to call
+   [set_loc_pos] to fix it. *)
+let bump_loc_line_last loc bol_pos =
+  let loc' =
+    Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos
+		  (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc)
+  in
+  Ploc.encl loc loc'
 
-let make_loc = Ploc.make_unlined
+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 =
+  let line_nb = Ploc.line_nb_last loc in
+  let bol_pos = Ploc.bol_pos_last loc in
+  Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos
+		(Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
 
 ELSE
 
@@ -44,16 +74,39 @@ module CompatLoc = Camlp4.PreCast.Loc
 
 exception Exc_located = CompatLoc.Exc_located
 
-let of_coqloc loc =
-  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
-  CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false)
-
 let to_coqloc loc =
-  Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc)
-    (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc)
+  { Loc.fname = CompatLoc.file_name loc;
+    Loc.line_nb = CompatLoc.start_line loc;
+    Loc.bol_pos = CompatLoc.start_bol loc;
+    Loc.bp = CompatLoc.start_off loc;
+    Loc.ep = CompatLoc.stop_off loc;
+    Loc.line_nb_last = CompatLoc.stop_line loc;
+    Loc.bol_pos_last = CompatLoc.stop_bol loc; }
+
+let make_loc fname line_nb bol_pos start stop =
+  CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
+
+open CompatLoc
+
+let set_loc_pos loc bp ep =
+  of_tuple (file_name loc, start_line loc, start_bol loc, bp,
+	    stop_line loc, stop_bol loc, ep, is_ghost loc)
+
+let bump_loc_line loc bol_pos =
+  of_tuple (file_name loc, start_line loc + 1, bol_pos, start_off loc,
+	    start_line loc + 1, bol_pos, stop_off loc, is_ghost loc)
 
-let make_loc (start, stop) =
-  CompatLoc.of_tuple ("", 0, 0, start, 0, 0, stop, false)
+let bump_loc_line_last loc bol_pos =
+  of_tuple (file_name loc, start_line loc, start_bol loc, start_off loc,
+	    stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc)
+
+let set_loc_file loc fname =
+  of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc,
+	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)
+
+let after loc =
+  of_tuple (file_name loc, stop_line loc, stop_bol loc, stop_off loc,
+	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)
 
 END
 
@@ -65,6 +118,7 @@ IFDEF CAMLP5 THEN
 
 module PcamlSig = struct end
 module Token = Token
+module CompatGramext = struct include Gramext type assoc = g_assoc end
 
 ELSE
 
@@ -73,69 +127,11 @@ module Ast = Camlp4.PreCast.Ast
 module Pcaml = Camlp4.PreCast.Syntax
 module MLast = Ast
 module Token = struct exception Error of string end
+module CompatGramext = Camlp4.Sig.Grammar
 
 END
 
-
-(** Grammar auxiliary types *)
-
-IFDEF CAMLP5 THEN
-
-let to_coq_assoc = function
-| Gramext.RightA -> Extend.RightA
-| Gramext.LeftA -> Extend.LeftA
-| Gramext.NonA -> Extend.NonA
-
-let of_coq_assoc = function
-| Extend.RightA -> Gramext.RightA
-| Extend.LeftA -> Gramext.LeftA
-| Extend.NonA -> Gramext.NonA
-
-let of_coq_position = function
-| Extend.First -> Gramext.First
-| Extend.Last -> Gramext.Last
-| Extend.Before s -> Gramext.Before s
-| Extend.After s -> Gramext.After s
-| Extend.Level s -> Gramext.Level s
-
-let to_coq_position = function
-| Gramext.First -> Extend.First
-| Gramext.Last -> Extend.Last
-| Gramext.Before s -> Extend.Before s
-| Gramext.After s -> Extend.After s
-| Gramext.Level s -> Extend.Level s
-| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *)
-
-ELSE
-
-let to_coq_assoc = function
-| PcamlSig.Grammar.RightA -> Extend.RightA
-| PcamlSig.Grammar.LeftA -> Extend.LeftA
-| PcamlSig.Grammar.NonA -> Extend.NonA
-
-let of_coq_assoc = function
-| Extend.RightA -> PcamlSig.Grammar.RightA
-| Extend.LeftA -> PcamlSig.Grammar.LeftA
-| Extend.NonA -> PcamlSig.Grammar.NonA
-
-let of_coq_position = function
-| Extend.First -> PcamlSig.Grammar.First
-| Extend.Last -> PcamlSig.Grammar.Last
-| Extend.Before s -> PcamlSig.Grammar.Before s
-| Extend.After s -> PcamlSig.Grammar.After s
-| Extend.Level s -> PcamlSig.Grammar.Level s
-
-let to_coq_position = function
-| PcamlSig.Grammar.First -> Extend.First
-| PcamlSig.Grammar.Last -> Extend.Last
-| PcamlSig.Grammar.Before s -> Extend.Before s
-| PcamlSig.Grammar.After s -> Extend.After s
-| PcamlSig.Grammar.Level s -> Extend.Level s
-
-END
-
-
-(** Signature of Lexer *)
+(** Signature of CLexer *)
 
 IFDEF CAMLP5 THEN
 
@@ -146,12 +142,23 @@ module type LexerSig = sig
     exception E of t
     val to_string : t -> string
   end
+  type lexer_state
+  val init_lexer_state : string option -> lexer_state
+  val set_lexer_state : lexer_state -> unit
+  val release_lexer_state : unit -> lexer_state
+  val drop_lexer_state : unit -> unit
 end
 
 ELSE
 
-module type LexerSig =
-  Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+module type LexerSig = sig
+  include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+  type lexer_state
+  val init_lexer_state : string option -> lexer_state
+  val set_lexer_state : lexer_state -> unit
+  val release_lexer_state : unit -> lexer_state
+  val drop_lexer_state : unit -> unit
+end
 
 END
 
@@ -170,10 +177,13 @@ module type GrammarSig = sig
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 end
@@ -189,16 +199,37 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable = parsable * L.lexer_state ref
+  let parsable ?file c =
+    let state = ref (L.init_lexer_state file) in
+    L.set_lexer_state !state;
+    let a = parsable c in
+    state := L.release_lexer_state ();
+    (a,state)
   let action = Gramext.action
   let entry_create = Entry.create
-  let entry_parse e p =
-    try Entry.parse e p
-    with Exc_located (loc,e) -> Loc.raise (to_coqloc loc) e
-IFDEF CAMLP5_6_02_1 THEN
+  let entry_parse e (p,state) =
+    L.set_lexer_state !state;
+    try
+      let c = Entry.parse e p in
+      state := L.release_lexer_state ();
+      c
+    with Exc_located (loc,e) ->
+      L.drop_lexer_state ();
+      let loc' = Loc.get_loc (Exninfo.info e) in
+      let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
+      Loc.raise loc e
+  let with_parsable (p,state) f x =
+    L.set_lexer_state !state;
+    try
+      let a = f x in
+      state := L.release_lexer_state ();
+      a
+    with e ->
+      L.drop_lexer_state ();
+      raise e
+
   let entry_print ft x = Entry.print ft x
-ELSE
-  let entry_print _ x = Entry.print x
-END
   let srules' = Gramext.srules
   let parse_tokens_after_filter = Entry.parse_token
 end
@@ -210,12 +241,13 @@ module type GrammarSig = sig
     with module Loc = CompatLoc and type Token.t = Tok.t
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable
-  val parsable : char Stream.t -> parsable
+  type coq_parsable
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
 end
 
@@ -225,19 +257,96 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   include Camlp4.Struct.Grammar.Static.Make (L)
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable = char Stream.t
-  let parsable s = s
+  type coq_parsable = char Stream.t * L.lexer_state ref
+  let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state)
   let action = Action.mk
   let entry_create = Entry.mk
-  let entry_parse e s =
-    try parse e (*FIXME*)CompatLoc.ghost s
-    with Exc_located (loc,e) -> raise_coq_loc loc e
+  let entry_parse e (s,state) =
+    L.set_lexer_state !state;
+    try
+      let c = parse e (*FIXME*)CompatLoc.ghost s in
+      state := L.release_lexer_state ();
+      c
+    with Exc_located (loc,e) ->
+      L.drop_lexer_state ();
+      raise_coq_loc loc e;;
+  let with_parsable (p,state) f x =
+    L.set_lexer_state !state;
+    try
+      let a = f x in
+      state := L.release_lexer_state ();
+      a
+    with e ->
+      L.drop_lexer_state ();
+      Pervasives.raise e;;
   let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
 
 END
 
+(** Some definitions are grammar-specific in Camlp4, so we use a functor to
+    depend on it while taking a dummy argument in Camlp5. *)
+
+module GramextMake (G : GrammarSig) :
+sig
+  val stoken : Tok.t -> G.symbol
+  val sself : G.symbol
+  val snext : G.symbol
+  val slist0 : G.symbol -> G.symbol
+  val slist0sep : G.symbol * G.symbol -> G.symbol
+  val slist1 : G.symbol -> G.symbol
+  val slist1sep : G.symbol * G.symbol -> G.symbol
+  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
+
+IFDEF CAMLP5 THEN
+  let stoken tok =
+    let pattern = match tok with
+    | Tok.KEYWORD s -> "", s
+    | Tok.IDENT s -> "IDENT", s
+    | Tok.PATTERNIDENT s -> "PATTERNIDENT", s
+    | Tok.FIELD s -> "FIELD", s
+    | 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
+ELSE
+  module Gramext = G
+  let stoken tok = match tok with
+  | Tok.KEYWORD s -> Gramext.Skeyword s
+  | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok)
+END
+
+  IFDEF CAMLP5 THEN
+     let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
+     let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
+  ELSE
+    let slist0sep (x, y) = Gramext.Slist0sep (x, y)
+    let slist1sep (x, y) = Gramext.Slist1sep (x, y)
+  END
+
+  let snterml (x, y) = Gramext.Snterml (x, y)
+  let snterm x = Gramext.Snterm x
+  let sself = Gramext.Sself
+  let snext = Gramext.Snext
+  let slist0 x = Gramext.Slist0 x
+  let slist1 x = Gramext.Slist1 x
+  let sopt x = Gramext.Sopt x
+
+  let snterml_level = function
+  | Gramext.Snterml (_, l) -> l
+  | _ -> failwith "snterml_level"
+
+end
+
 
 (** Misc functional adjustments *)
 
@@ -303,23 +412,10 @@ let make_fun loc cl =
 
 END
 
-(** Explicit antiquotation $anti:... $ *)
-
-IFDEF CAMLP5 THEN
-let expl_anti loc e = <:expr< $anti:e$ >>
-ELSE
-let expl_anti _loc e = e (* FIXME: understand someday if we can do better *)
-END
-
-(** Qualified names in OCaml *)
-
 IFDEF CAMLP5 THEN
-let qualified_name loc path name =
-  let fold dir accu = <:expr< $uid:dir$.$accu$ >> in
-  List.fold_right fold path <:expr< $lid:name$ >>
+let warning_verbose = Gramext.warning_verbose
 ELSE
-let qualified_name loc path name =
-  let fold dir accu = Ast.IdAcc (loc, Ast.IdUid (loc, dir), accu) in
-  let path = List.fold_right fold path (Ast.IdLid (loc, name)) in
-  Ast.ExId (loc, path)
+(* TODO: this is a workaround, since there isn't such
+   [warning_verbose] in new camlp4. *)
+let warning_verbose = ref true
 END
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index b0bbdd81..a292c746 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -6,17 +6,145 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
-open Errors
+open CErrors
 open Util
 open Pcoq
-open Extend
 open Constrexpr
+open Notation
 open Notation_term
+open Extend
 open Libnames
-open Tacexpr
 open Names
-open Egramml
+
+(**********************************************************************)
+(* This determines (depending on the associativity of the current
+   level and on the expected associativity) if a reference to constr_n is
+   a reference to the current level (to be translated into "SELF" on the
+   left border and into "constr LEVEL n" elsewhere), to the level below
+   (to be translated into "NEXT") or to an below wrt associativity (to be
+   translated in camlp4 into "constr" without level) or to another level
+   (to be translated into "constr LEVEL n")
+
+   The boolean is true if the entry was existing _and_ empty; this to
+   circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the
+   converse of the extension mechanism *)
+
+let constr_level = string_of_int
+
+let default_levels =
+  [200,Extend.RightA,false;
+   100,Extend.RightA,false;
+   99,Extend.RightA,true;
+   10,Extend.RightA,false;
+   9,Extend.RightA,false;
+   8,Extend.RightA,true;
+   1,Extend.LeftA,false;
+   0,Extend.RightA,false]
+
+let default_pattern_levels =
+  [200,Extend.RightA,true;
+   100,Extend.RightA,false;
+   99,Extend.RightA,true;
+   11,Extend.LeftA,false;
+   10,Extend.RightA,false;
+   1,Extend.LeftA,false;
+   0,Extend.RightA,false]
+
+let default_constr_levels = (default_levels, default_pattern_levels)
+
+(* At a same level, LeftA takes precedence over RightA and NoneA *)
+(* In case, several associativity exists for a level, we make two levels, *)
+(* first LeftA, then RightA and NoneA together *)
+
+let admissible_assoc = function
+  | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false
+  | Extend.RightA, Some Extend.LeftA -> false
+  | _ -> true
+
+let create_assoc = function
+  | None -> Extend.RightA
+  | Some a -> a
+
+let error_level_assoc p current expected =
+  let open Pp in
+  let pr_assoc = function
+    | Extend.LeftA -> str "left"
+    | Extend.RightA -> str "right"
+    | Extend.NonA -> str "non" in
+  errorlabstrm ""
+    (str "Level " ++ int p ++ str " is already declared " ++
+     pr_assoc current ++ str " associative while it is now expected to be " ++
+     pr_assoc expected ++ str " associative.")
+
+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 ->
+      current, (None, None, None, None)
+  | Some n ->
+      let after = ref None in
+      let init = ref None in
+      let rec add_level q = function
+        | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
+        | (p,a,reinit)::l when Int.equal p n ->
+            if reinit then
+	      let a' = create_assoc assoc in
+              (init := Some (a',create_pos q); (p,a',false)::l)
+	    else if admissible_assoc (a,assoc) then
+	      raise Exit
+            else
+	      error_level_assoc p a (Option.get assoc)
+	| l -> after := q; (n,create_assoc assoc,ensure)::l
+      in
+      try
+	let updated = add_level None current in
+	let assoc = create_assoc assoc in
+        begin match !init with
+        | None ->
+	  (* Create the entry *)
+	   updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
+        | _ ->
+	  (* The reinit flag has been updated *)
+	   updated, (Some (Extend.Level (constr_level n)), None, None, !init)
+        end
+      with
+	  (* Nothing has changed *)
+          Exit ->
+	    (* Just inherit the existing associativity and name (None) *)
+	    current, (Some (Extend.Level (constr_level n)), None, None, None)
+
+let rec list_mem_assoc_triple x = function
+  | [] -> false
+  | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l
+
+let register_empty_levels accu forpat levels =
+  let rec filter accu = function
+  | [] -> ([], accu)
+  | n :: rem ->
+    let rem, accu = filter accu rem in
+    let (clev, plev) = accu in
+    let levels = if forpat then plev else clev in
+    if not (list_mem_assoc_triple n levels) then
+      let nlev, ans = find_position_gen levels true None (Some n) in
+      let nlev = if forpat then (clev, nlev) else (nlev, plev) in
+      ans :: rem, nlev
+    else rem, accu
+  in
+  filter accu levels
+
+let find_position accu forpat assoc level =
+  let (clev, plev) = accu in
+  let levels = if forpat then plev else clev in
+  let nlev, ans = find_position_gen levels false assoc level in
+  let nlev = if forpat then (clev, nlev) else (nlev, plev) in
+  (ans, nlev)
 
 (**************************************************************************)
 (*
@@ -45,6 +173,146 @@ open Egramml
 (**********************************************************************)
 (** Declare Notations grammar rules                                   *)
 
+(**********************************************************************)
+(* Binding constr entry keys to entries                               *)
+
+(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
+let camlp4_assoc = function
+  | Some NonA | Some RightA -> RightA
+  | None | Some LeftA -> LeftA
+
+let assoc_eq al ar = match al, ar with
+| NonA, NonA
+| RightA, RightA
+| LeftA, LeftA -> true
+| _, _ -> false
+
+(* [adjust_level assoc from prod] where [assoc] and [from] are the name
+   and associativity of the level where to add the rule; the meaning of
+   the result is
+
+     None = SELF
+     Some None = NEXT
+     Some (Some (n,cur)) = constr LEVEL n
+         s.t. if [cur] is set then [n] is the same as the [from] level *)
+let adjust_level assoc from = function
+(* Associativity is None means force the level *)
+  | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
+(* Compute production name on the right side *)
+  (* If NonA or LeftA on the right-hand side, set to NEXT *)
+  | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) ->
+      Some None
+  (* If RightA on the right-hand side, set to the explicit (current) level *)
+  | (NumLevel n,BorderProd (Right,Some RightA)) ->
+      Some (Some (n,true))
+(* Compute production name on the left side *)
+  (* If NonA on the left-hand side, adopt the current assoc ?? *)
+  | (NumLevel n,BorderProd (Left,Some NonA)) -> None
+  (* If the expected assoc is the current one, set to SELF *)
+  | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) ->
+      None
+  (* Otherwise, force the level, n or n-1, according to expected assoc *)
+  | (NumLevel n,BorderProd (Left,Some a)) ->
+    begin match a with
+    | LeftA -> Some (Some (n, true))
+    | _ -> Some None
+    end
+  (* None means NEXT *)
+  | (NextLevel,_) -> Some None
+(* Compute production name elsewhere *)
+  | (NumLevel n,InternalProd) ->
+    if from = n + 1 then Some None else Some (Some (n, Int.equal n from))
+
+type _ target =
+| ForConstr : constr_expr target
+| ForPattern : cases_pattern_expr target
+
+type prod_info = production_level * production_position
+
+type (_, _) entry =
+| TTName : ('self, Name.t Loc.located) entry
+| TTReference : ('self, reference) entry
+| TTBigint : ('self, Bigint.bigint) entry
+| TTBinder : ('self, local_binder list) entry
+| TTConstr : prod_info * 'r target -> ('r, 'r) entry
+| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
+| TTBinderListT : ('self, local_binder list) entry
+| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry
+
+type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
+
+(* This computes the name of the level where to add a new rule *)
+let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option =
+  fun forpat level -> match forpat with
+  | ForConstr ->
+    if level = 200 then Constr.binder_constr, None
+    else Constr.operconstr, Some level
+  | ForPattern -> Constr.pattern, Some level
+
+let target_entry : type s. s target -> s Gram.entry = function
+| ForConstr -> Constr.operconstr
+| ForPattern -> Constr.pattern
+
+let is_self from e = match e with
+| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
+| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n
+| _ -> false
+
+let is_binder_level from e = match e with
+| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200
+| _ -> false
+
+let make_sep_rules tkl =
+  let rec mkrule : Tok.t list -> unit rules = function
+  | [] -> Rules ({ norec_rule = Stop }, ignore)
+  | tkn :: rem ->
+    let Rules ({ norec_rule = r }, f) = mkrule rem in
+    let r = { norec_rule = Next (r, Atoken tkn) } in
+    Rules (r, fun _ -> f)
+  in
+  let r = mkrule (List.rev tkl) in
+  Arules [r]
+
+let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat ->
+  if is_binder_level from p then Aentryl (target_entry forpat, 200)
+  else if is_self from p then Aself
+  else
+    let g = target_entry forpat in
+    let lev = adjust_level assoc from p in
+    begin match lev with
+    | None -> Aentry g
+    | Some None -> Anext
+    | Some (Some (lev, cur)) -> Aentryl (g, lev)
+    end
+
+let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
+| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat
+| TTConstrList (typ', [], forpat) ->
+  Alist1 (symbol_of_target typ' assoc from forpat)
+| TTConstrList (typ', tkl, forpat) ->
+  Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
+| TTBinderListF [] -> Alist1 (Aentry Constr.binder)
+| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
+| TTName -> Aentry Prim.name
+| TTBinder -> Aentry Constr.binder
+| TTBinderListT -> Aentry Constr.open_binders
+| TTBigint -> Aentry Prim.bigint
+| TTReference -> Aentry Constr.global
+
+let interp_entry forpat e = match e with
+| ETName -> TTAny TTName
+| ETReference -> TTAny TTReference
+| ETBigint -> TTAny TTBigint
+| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList")
+| ETBinder false  -> TTAny TTBinder
+| ETConstr p -> TTAny (TTConstr (p, forpat))
+| ETPattern -> assert false (** not used *)
+| ETOther _ -> assert false (** not used *)
+| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETBinderList (true, []) -> TTAny TTBinderListT
+| ETBinderList (true, _) -> assert false
+| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl)
+
 let constr_expr_of_name (loc,na) = match na with
   | Anonymous -> CHole (loc,None,Misctypes.IntroAnonymous,None)
   | Name id -> CRef (Ident (loc,id), None)
@@ -53,333 +321,158 @@ let cases_pattern_expr_of_name (loc,na) = match na with
   | Anonymous -> CPatAtom (loc,None)
   | Name id -> CPatAtom (loc,Some (Ident (loc,id)))
 
-type grammar_constr_prod_item =
-  | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
-  | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items;
-       concat with last parsed list if true *)
-
-let make_constr_action
-  (f : Loc.t -> constr_notation_substitution -> constr_expr) pil =
-  let rec make (constrs,constrlists,binders as fullsubst) = function
-  | [] ->
-      Gram.action (fun (loc:CompatLoc.t) -> f (!@loc) fullsubst)
-  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
-      (* parse a non-binding item *)
-      Gram.action (fun _ -> make fullsubst tl)
-  | GramConstrNonTerminal (typ, Some _) :: tl ->
-      (* parse a binding non-terminal *)
-    (match typ with
-    | (ETConstr _| ETOther _) ->
-	Gram.action (fun (v:constr_expr) ->
-	  make (v :: constrs, constrlists, binders) tl)
-    | ETReference ->
-        Gram.action (fun (v:reference) ->
-	  make (CRef (v,None) :: constrs, constrlists, binders) tl)
-    | ETName ->
-        Gram.action (fun (na:Loc.t * Name.t) ->
-	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
-    | ETBigint ->
-        Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPrim(Loc.ghost,Numeral v) :: constrs, constrlists, binders) tl)
-    | ETConstrList (_,n) ->
-	Gram.action (fun (v:constr_expr list) ->
-	  make (constrs, v::constrlists, binders) tl)
-    | ETBinder _ | ETBinderList (true,_) ->
-	Gram.action (fun (v:local_binder list) ->
-	  make (constrs, constrlists, v::binders) tl)
-    | ETBinderList (false,_) ->
-	Gram.action (fun (v:local_binder list list) ->
-	  make (constrs, constrlists, List.flatten v::binders) tl)
-    | ETPattern ->
-	failwith "Unexpected entry of type cases pattern")
-  | GramConstrListMark (n,b) :: tl ->
-      (* Rebuild expansions of ConstrList *)
-      let heads,constrs = List.chop n constrs in
-      let constrlists =
-	if b then (heads@List.hd constrlists)::List.tl constrlists
-	else heads::constrlists
-      in make (constrs, constrlists, binders) tl
-  in
-  make ([],[],[]) (List.rev pil)
-
-let check_cases_pattern_env loc (env,envlist,hasbinders) =
-  if hasbinders then Topconstr.error_invalid_pattern_notation loc
-  else (env,envlist)
-
-let make_cases_pattern_action
-  (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
-  let rec make (env,envlist,hasbinders as fullenv) = function
-  | [] ->
-      Gram.action
-	(fun (loc:CompatLoc.t) ->
-	  let loc = !@loc in
-	  f loc (check_cases_pattern_env loc fullenv))
-  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
-      (* parse a non-binding item *)
-      Gram.action (fun _ -> make fullenv tl)
-  | GramConstrNonTerminal (typ, Some _) :: tl ->
-      (* parse a binding non-terminal *)
-    (match typ with
-    | ETConstr _ -> (* pattern non-terminal *)
-        Gram.action (fun (v:cases_pattern_expr) ->
-          make (v::env, envlist, hasbinders) tl)
-    | ETReference ->
-        Gram.action (fun (v:reference) ->
-	  make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl)
-    | ETName ->
-        Gram.action (fun (na:Loc.t * Name.t) ->
-	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
-    | ETBigint ->
-        Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (Loc.ghost,Numeral v) :: env, envlist, hasbinders) tl)
-    | ETConstrList (_,_) ->
-        Gram.action  (fun (vl:cases_pattern_expr list) ->
-	  make (env, vl :: envlist, hasbinders) tl)
-    | ETBinder _ | ETBinderList (true,_) ->
-	Gram.action (fun (v:local_binder list) ->
-	  make (env, envlist, hasbinders) tl)
-    | ETBinderList (false,_) ->
-	Gram.action (fun (v:local_binder list list) ->
-	  make (env, envlist, true) tl)
-    | (ETPattern | ETOther _) ->
-        anomaly (Pp.str "Unexpected entry of type cases pattern or other"))
-  | GramConstrListMark (n,b) :: tl ->
-      (* Rebuild expansions of ConstrList *)
-      let heads,env = List.chop n env in
-      if b then
-        make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
-      else
-        make (env,heads::envlist,hasbinders) tl
-  in
-  make ([],[],false) (List.rev pil)
-
-let rec make_constr_prod_item assoc from forpat = function
-  | GramConstrTerminal tok :: l ->
-      gram_token_of_token tok :: make_constr_prod_item assoc from forpat l
-  | GramConstrNonTerminal (nt, ovar) :: l ->
-      symbol_of_constr_prod_entry_key assoc from forpat nt
-      :: make_constr_prod_item assoc from forpat l
-  | GramConstrListMark _ :: l ->
-      make_constr_prod_item assoc from forpat l
-  | [] ->
-      []
-
-let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
-  let entry =
-    if forpat then weaken_entry Constr.pattern
-    else weaken_entry Constr.operconstr in
-  grammar_extend entry reinit (pos,[(name, p4assoc, [])])
-
-let pure_sublevels level symbs =
-  let filter s =
-    try
-      let i = level_of_snterml s in
-      begin match level with
-      | Some j when Int.equal i j -> None
-      | _ -> Some i
-      end
-    with Failure _ -> None
-  in
-  List.map_filter filter symbs
-
-let extend_constr (entry,level) (n,assoc) mkact forpat rules =
-  List.fold_left (fun nb pt ->
-  let symbs = make_constr_prod_item assoc n forpat pt in
-  let pure_sublevels = pure_sublevels level symbs in
-  let needed_levels = register_empty_levels forpat pure_sublevels in
-  let map_level (pos, ass1, name, ass2) =
-    (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in
-  let needed_levels = List.map map_level needed_levels in
-  let pos,p4assoc,name,reinit = find_position forpat assoc level in
-  let nb_decls = List.length needed_levels + 1 in
-  List.iter (prepare_empty_levels forpat) needed_levels;
-  grammar_extend entry reinit (Option.map of_coq_position pos,
-    [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]);
-  nb_decls) 0 rules
-
-type notation_grammar = {
-  notgram_level : int;
-  notgram_assoc : gram_assoc option;
-  notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
-}
-
-let extend_constr_constr_notation ng =
-  let level = ng.notgram_level in
-  let mkact loc env = CNotation (loc, ng.notgram_notation, env) in
-  let e = interp_constr_entry_key false (ETConstr (level, ())) in
-  let ext = (ETConstr (level, ()), ng.notgram_assoc) in
-  extend_constr e ext (make_constr_action mkact) false ng.notgram_prods
-
-let extend_constr_pat_notation ng =
-  let level = ng.notgram_level in
-  let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in
-  let e = interp_constr_entry_key true (ETConstr (level, ())) in
-  let ext = ETConstr (level, ()), ng.notgram_assoc in
-  extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
-
-let extend_constr_notation ng =
-  (* Add the notation in constr *)
-  let nb = extend_constr_constr_notation ng in
-  (* Add the notation in cases_pattern *)
-  let nb' = extend_constr_pat_notation ng in
-  nb + nb'
-
-(**********************************************************************)
-(** Grammar declaration for Tactic Notation (Coq level)               *)
-
-let get_tactic_entry n =
-  if Int.equal n 0 then
-    weaken_entry Tactic.simple_tactic, None
-  else if Int.equal n 5 then
-    weaken_entry Tactic.binder_tactic, None
-  else if 1<=n && n<5 then
-    weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
-  else
-    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
-
-(**********************************************************************)
-(** State of the grammar extensions                                   *)
-
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : grammar_prod_item list;
+type 'r env = {
+  constrs : 'r list;
+  constrlists : 'r list list;
+  binders : (local_binder list * bool) list;
 }
 
-type all_grammar_command =
-  | Notation of Notation.level * notation_grammar
-  | TacticGrammar of KerName.t * tactic_grammar
-  | MLTacticGrammar of ml_tactic_name * grammar_prod_item list list
-
-(** ML Tactic grammar extensions *)
-
-let add_ml_tactic_entry name prods =
-  let entry = weaken_entry Tactic.simple_tactic in
-  let mkact loc l : raw_tactic_expr = Tacexpr.TacML (loc, name, List.map snd l) in
-  let rules = List.map (make_rule mkact) prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (None ,[(None, None, List.rev rules)]);
-  1
-
-(* Declaration of the tactic grammar rule *)
-
-let head_is_ident tg = match tg.tacgram_prods with
-| GramTerminal _::_ -> true
-| _ -> false
-
-(** Tactic grammar extensions *)
-
-let add_tactic_entry kn tg =
-  let entry, pos = get_tactic_entry tg.tacgram_level in
-  let mkact loc l = (TacAlias (loc,kn,l):raw_tactic_expr) in
-  let () =
-    if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
-      error "Notation for simple tactic must start with an identifier."
-  in
-  let rules = make_rule mkact tg.tacgram_prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
-  1
-
-let (grammar_state : (int * all_grammar_command) list ref) = ref []
-
-let extend_grammar gram =
-  let nb = match gram with
-  | Notation (_,a) -> extend_constr_notation a
-  | TacticGrammar (kn, g) -> add_tactic_entry kn g
-  | MLTacticGrammar (name, pr) -> add_ml_tactic_entry name pr
+let push_constr subst v = { subst with constrs = v :: subst.constrs }
+
+let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v ->
+match e with
+| TTConstr _ -> push_constr subst v
+| TTName ->
+  begin match forpat with
+  | ForConstr -> push_constr subst (constr_expr_of_name v)
+  | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
+  end
+| TTBinder -> { subst with binders = (v, true) :: subst.binders }
+| TTBinderListT -> { subst with binders = (v, true) :: subst.binders }
+| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
+| TTBigint ->
+  begin match forpat with
+  | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v))
+  | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v))
+  end
+| TTReference ->
+  begin match forpat with
+  | ForConstr -> push_constr subst (CRef (v, None))
+  | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v))
+  end
+| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
+
+type (_, _) ty_symbol =
+| TyTerm : Tok.t -> ('s, string) ty_symbol
+| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol
+
+type ('self, _, 'r) ty_rule =
+| TyStop : ('self, 'r, 'r) ty_rule
+| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule
+| TyMark : int * bool * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule
+
+type 'r gen_eval = Loc.t -> 'r env -> 'r
+
+let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> a = function
+| TyStop ->
+  fun f env loc -> f loc env
+| TyNext (rem, TyTerm _) ->
+  fun f env _ -> ty_eval rem f env
+| TyNext (rem, TyNonTerm (_, _, _, false)) ->
+  fun f env _ -> ty_eval rem f env
+| TyNext (rem, TyNonTerm (forpat, e, _, true)) ->
+  fun f env v ->
+    ty_eval rem f (push_item forpat e env v)
+| TyMark (n, b, rem) ->
+  fun f env ->
+    let heads, constrs = List.chop n env.constrs in
+    let constrlists =
+      if b then (heads @ List.hd env.constrlists) :: List.tl env.constrlists
+      else heads :: env.constrlists
+    in
+    ty_eval rem f { env with constrs; constrlists; } 
+
+let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
+| TyStop -> Stop
+| TyMark (_, _, r) -> ty_erase r
+| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok)
+| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s)
+
+type ('self, 'r) any_ty_rule =
+| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
+
+let make_ty_rule assoc from forpat prods =
+  let rec make_ty_rule = function
+  | [] -> AnyTyRule TyStop
+  | GramConstrTerminal tok :: rem ->
+    let AnyTyRule r = make_ty_rule rem in
+    AnyTyRule (TyNext (r, TyTerm tok))
+  | GramConstrNonTerminal (e, var) :: rem ->
+    let AnyTyRule r = make_ty_rule rem in
+    let TTAny e = interp_entry forpat e in
+    let s = symbol_of_entry assoc from e in
+    let bind = match var with None -> false | Some _ -> true in
+    AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind)))
+  | GramConstrListMark (n, b) :: rem ->
+    let AnyTyRule r = make_ty_rule rem in
+    AnyTyRule (TyMark (n, b, r))
   in
-  grammar_state := (nb,gram) :: !grammar_state
+  make_ty_rule (List.rev prods)
 
-let extend_constr_grammar pr ntn =
-  extend_grammar (Notation (pr, ntn))
+let target_to_bool : type r. r target -> bool = function
+| ForConstr -> false
+| ForPattern -> true
 
-let extend_tactic_grammar kn ntn =
-  extend_grammar (TacticGrammar (kn, ntn))
+let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
+  let empty = (pos, [(name, p4assoc, [])]) in
+  if forpat then ExtendRule (Constr.pattern, reinit, empty)
+  else ExtendRule (Constr.operconstr, reinit, empty)
+
+let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with
+| Stop -> []
+| Next (rem, Aentryl (_, i)) ->
+  let rem = pure_sublevels level rem in
+  begin match level with
+  | Some j when Int.equal i j -> rem
+  | _ -> i :: rem
+  end
+| Next (rem, _) -> pure_sublevels level rem
+
+let make_act : type r. r target -> _ -> r gen_eval = function
+| ForConstr -> fun notation loc env ->
+  let env = (env.constrs, env.constrlists, List.map fst env.binders) in
+  CNotation (loc, notation , env)
+| ForPattern -> fun notation loc env ->
+  let invalid = List.exists (fun (_, b) -> not b) env.binders in
+  let () = if invalid then Topconstr.error_invalid_pattern_notation loc in
+  let env = (env.constrs, env.constrlists) in
+  CPatNotation (loc, notation, env, [])
+
+let extend_constr state forpat ng =
+  let n = ng.notgram_level in
+  let assoc = ng.notgram_assoc in
+  let (entry, level) = interp_constr_entry_key forpat n in
+  let fold (accu, state) pt =
+    let AnyTyRule r = make_ty_rule assoc n forpat pt in
+    let symbs = ty_erase r in
+    let pure_sublevels = pure_sublevels level symbs in
+    let isforpat = target_to_bool forpat in
+    let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
+    let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
+    let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
+    let empty = { constrs = []; constrlists = []; binders = [] } in
+    let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
+    let rule = (name, p4assoc, [Rule (symbs, act)]) in
+    let r = ExtendRule (entry, reinit, (pos, [rule])) in
+    (accu @ empty_rules @ [r], state)
+  in
+  List.fold_left fold ([], state) ng.notgram_prods
 
-let extend_ml_tactic_grammar name ntn =
-  extend_grammar (MLTacticGrammar (name, ntn))
+let constr_levels = GramState.field ()
 
-let recover_constr_grammar ntn prec =
-  let filter = function
-  | _, Notation (prec', ng) when
-      Notation.level_eq prec prec' &&
-      String.equal ntn ng.notgram_notation -> Some ng
-  | _ -> None
+let extend_constr_notation (_, ng) state =
+  let levels = match GramState.get state constr_levels with
+  | None -> default_constr_levels
+  | Some lev -> lev
   in
-  match List.map_filter filter !grammar_state with
-  | [x] -> x
-  | _ -> assert false
-
-(* Summary functions: the state of the lexer is included in that of the parser.
-   Because the grammar affects the set of keywords when adding or removing
-   grammar rules. *)
-type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
-
-let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
-
-(* We compare the current state of the grammar and the state to unfreeze,
-   by computing the longest common suffixes *)
-let factorize_grams l1 l2 =
-  if l1 == l2 then ([], [], l1) else List.share_tails l1 l2
-
-let number_of_entries gcl =
-  List.fold_left (fun n (p,_) -> n + p) 0 gcl
-
-let unfreeze (grams, lex) =
-  let (undo, redo, common) = factorize_grams !grammar_state grams in
-  let n = number_of_entries undo in
-  remove_grammars n;
-  remove_levels n;
-  grammar_state := common;
-  Lexer.unfreeze lex;
-  List.iter extend_grammar (List.rev_map snd redo)
-
-(** No need to provide an init function : the grammar state is
-    statically available, and already empty initially, while
-    the lexer state should not be resetted, since it contains
-    keywords declared in g_*.ml4 *)
-
-let _ =
-  Summary.declare_summary "GRAMMAR_LEXER"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = Summary.nop }
-
-let with_grammar_rule_protection f x =
-  let fs = freeze false in
-  try let a = f x in unfreeze fs; a
-  with reraise ->
-    let reraise = Errors.push reraise in
-    let () = unfreeze fs in
-    iraise reraise
-
-(**********************************************************************)
-(** Ltac quotations                                                   *)
+  (* Add the notation in constr *)
+  let (r, levels) = extend_constr levels ForConstr ng in
+  (* Add the notation in cases_pattern *)
+  let (r', levels) = extend_constr levels ForPattern ng in
+  let state = GramState.set state constr_levels levels in
+  (r @ r', state)
 
-let ltac_quotations = ref String.Set.empty
+let constr_grammar : (Notation.level * notation_grammar) grammar_command =
+  create_grammar_command "Notation" extend_constr_notation
 
-let create_ltac_quotation name cast wit e =
-  let () =
-    if String.Set.mem name !ltac_quotations then
-      failwith ("Ltac quotation " ^ name ^ " already registered")
-  in
-  let () = ltac_quotations := String.Set.add name !ltac_quotations in
-(*   let level = Some "1" in *)
-  let level = None in
-  let assoc = Some (of_coq_assoc Extend.RightA) in
-  let rule = [
-    gram_token_of_string name;
-    gram_token_of_string ":";
-    symbol_of_prod_entry_key (Agram (Gram.Entry.name e));
-  ] in
-  let action v _ _ loc =
-    let loc = !@loc in
-    let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in
-    TacArg (loc, arg)
-  in
-  let gram = (level, assoc, [rule, Gram.action action]) in
-  maybe_uncurry (Gram.extend Tactic.tactic_expr) (None, [gram])
+let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn)
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 964bd541..6dda3817 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -19,51 +19,7 @@ open Egramml
 (** This is the part specific to Coq-level Notation and Tactic Notation.
     For the ML-level tactic and vernac extensions, see Egramml. *)
 
-(** For constr notations *)
-
-type grammar_constr_prod_item =
-  | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
-  | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items;
-       concat with last parsed list if true *)
-
-type notation_grammar = {
-  notgram_level : int;
-  notgram_assoc : gram_assoc option;
-  notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
-}
-
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : grammar_prod_item list;
-}
-
 (** {5 Adding notations} *)
 
-val extend_constr_grammar : Notation.level -> notation_grammar -> unit
+val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
-
-val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
-(** Add a tactic notation rule to the parsing system. This produces a TacAlias
-    tactic with the provided kernel name. *)
-
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> grammar_prod_item list list -> unit
-(** Add a ML tactic notation rule to the parsing system. This produces a
-    TacML tactic with the provided string as name. *)
-
-val recover_constr_grammar : notation -> Notation.level -> notation_grammar
-(** For a declared grammar, returns the rule + the ordered entry types
-    of variables in the rule (for use in the interpretation) *)
-
-val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-
-(** {5 Adding tactic quotations} *)
-
-val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) ->
-  ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit
-(** [create_ltac_quotation name f wit e] adds a quotation rule to Ltac, that is,
-    Ltac grammar now accepts arguments of the form ["name" ":" <e>], and
-    generates a generic argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 3896970c..97a3e89a 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -7,41 +7,60 @@
 (************************************************************************)
 
 open Util
-open Compat
-open Names
+open Extend
 open Pcoq
 open Genarg
 open Vernacexpr
 
-(** Making generic actions in type generic_argument *)
-
-let make_generic_action
-  (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil =
-  let rec make env = function
-    | [] ->
-	Gram.action (fun loc -> f (to_coqloc loc) env)
-    | None :: tl -> (* parse a non-binding item *)
-        Gram.action (fun _ -> make env tl)
-    | Some (p, t) :: tl -> (* non-terminal *)
-        Gram.action (fun v -> make ((p, Unsafe.inj t v) :: env) tl) in
-  make [] (List.rev pil)
-
 (** Grammar extensions declared at ML level *)
 
-type grammar_prod_item =
+type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal of
-      Loc.t * argument_type * prod_entry_key * Id.t option
+  | GramNonTerminal :
+      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
+
+type 'a ty_arg = ('a -> raw_generic_argument)
+
+type ('self, _, 'r) ty_rule =
+| TyStop : ('self, 'r, 'r) ty_rule
+| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option ->
+  ('self, 'b -> 'a, 'r) ty_rule
+
+type ('self, 'r) any_ty_rule =
+| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
+
+let rec ty_rule_of_gram = function
+| [] -> AnyTyRule TyStop
+| GramTerminal s :: rem ->
+  let AnyTyRule rem = ty_rule_of_gram rem in
+  let tok = Atoken (CLexer.terminal s) in
+  let r = TyNext (rem, tok, None) in
+  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 r = TyNext (rem, tok, inj) in
+  AnyTyRule r
+
+let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
+| TyStop -> Extend.Stop
+| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
+
+type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
 
-let make_prod_item = function
-  | GramTerminal s -> (gram_token_of_string s, None)
-  | GramNonTerminal (_,t,e,po) ->
-      (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po)
+let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
+| TyStop -> fun f loc -> f loc []
+| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
+| TyNext (rem, tok, Some inj) -> fun f x ->
+  let f loc args = f loc (inj x :: args) in
+  ty_eval rem f
 
-let make_rule mkact pt =
-  let (symbs,ntl) = List.split (List.map make_prod_item pt) in
-  let act = make_generic_action mkact ntl in
-  (symbs, act)
+let make_rule f prod =
+  let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in
+  let symb = ty_erase ty_rule in
+  let f loc l = f loc (List.rev l) in
+  let act = ty_eval ty_rule f in
+  Extend.Rule (symb, act)
 
 (** Vernac grammar extensions *)
 
@@ -58,6 +77,6 @@ let get_extend_vernac_rule (s, i) =
 let extend_vernac_command_grammar s nt gl =
   let nt = Option.default Vernac_.command nt in
   vernac_exts := (s,gl) :: !vernac_exts;
-  let mkact loc l = VernacExtend (s,List.map snd l) in
+  let mkact loc l = VernacExtend (s, l) in
   let rules = [make_rule mkact gl] in
-  maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])
+  grammar_extend nt None (None, [None, None, rules])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index f71c368a..1ad94720 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -6,24 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Vernacexpr
+
 (** Mapping of grammar productions to camlp4 actions. *)
 
 (** This is the part specific to vernac extensions.
     For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
 
-type grammar_prod_item =
+type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal of Loc.t * Genarg.argument_type *
-      Pcoq.prod_entry_key * Names.Id.t option
+  | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
+      ('s, 'a) Extend.symbol -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
-    grammar_prod_item list -> unit
+  Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+    vernac_expr grammar_prod_item list -> unit
 
-val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list
+val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
 
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
-  (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) ->
-  grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
+  (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
+  'a grammar_prod_item list -> 'a Extend.production_rule
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5edb7b80..7f3a3d10 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -29,7 +29,7 @@ let constr_kw =
     "Prop"; "Set"; "Type"; ".("; "_"; "..";
     "`{"; "`("; "{|"; "|}" ]
 
-let _ = List.iter Lexer.add_keyword constr_kw
+let _ = List.iter CLexer.add_keyword constr_kw
 
 let mk_cast = function
     (c,(_,None)) -> c
@@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
-    Errors.user_err_loc
+    CErrors.user_err_loc
       (aloc,"Constr:mk_cofixb",
        Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
@@ -127,15 +127,12 @@ 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;
   Constr.ident:
-    [ [ id = Prim.ident -> id
-
-      (* This is used in quotations and Syntax *)
-      | id = METAIDENT -> Id.of_string id ] ]
+    [ [ id = Prim.ident -> id ] ]
   ;
   Prim.name:
     [ [ "_" -> (!@loc, Anonymous) ] ]
@@ -218,16 +215,13 @@ GEXTEND Gram
 	  CGeneralization (!@loc, Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
 	  CGeneralization (!@loc, Explicit, None, c)
-      | "ltac:"; "("; tac = Tactic.tactic_expr; ")" ->
+      | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" ->
           let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
           CHole (!@loc, None, IntroAnonymous, Some arg)
       ] ]
   ;
   record_declaration:
-    [ [ fs = record_fields -> CRecord (!@loc, None, fs)
-(*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
-(* 	  CRecord (!@loc, Some c, fs) *)
-    ] ]
+    [ [ fs = record_fields -> CRecord (!@loc, fs) ] ]
   ;
 
   record_fields:
@@ -267,14 +261,14 @@ GEXTEND Gram
           CLetTuple (!@loc,lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, None, [(c1,(None,None))], [(!@loc, [(!@loc,[p])], c2)])
+	    CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)])
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -304,10 +298,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
@@ -338,11 +332,10 @@ GEXTEND Gram
         br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ]
   ;
   case_item:
-    [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
-  ;
-  pred_pattern:
-    [ [ ona = OPT ["as"; id=name -> id];
-        ty = OPT ["in"; t=pattern -> t] -> (ona,ty) ] ]
+    [ [ c=operconstr LEVEL "100";
+        ona = OPT ["as"; id=name -> id];
+	ty = OPT ["in"; t=pattern -> t] ->
+	   (c,ona,ty) ] ]
   ;
   case_type:
     [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
@@ -386,14 +379,17 @@ GEXTEND Gram
     | "10" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
-	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp)
+	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
+	  | CPatCstr (_, r, None, l2) -> CErrors.user_err_loc
+              (cases_pattern_expr_loc p, "compound_pattern",
+               Pp.str "Nested applications not supported.")
 	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
 	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
-          | _ -> Errors.user_err_loc
+          | _ -> CErrors.user_err_loc
               (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Such pattern cannot have arguments."))
-      |"@"; r = Prim.reference; lp = LIST1 NEXT ->
-        CPatCstr (!@loc, r, lp, []) ]
+      |"@"; r = Prim.reference; lp = LIST0 NEXT ->
+        CPatCstr (!@loc, r, Some lp, []) ]
     | "1" LEFTA
       [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
     | "0"
@@ -405,6 +401,14 @@ GEXTEND Gram
               CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CPatNotation(!@loc,"( _ )",([p],[]),[])
             | _ -> p)
+      | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
+          let p =
+            match p with
+              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
+                CPatNotation(!@loc,"( _ )",([p],[]),[])
+            | _ -> p
+          in
+	  CPatCast (!@loc, p, ty)
       | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n))
       | s = string -> CPatPrim (!@loc, String s) ] ]
   ;
@@ -480,6 +484,13 @@ GEXTEND Gram
 	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
 	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+      | "'"; p = pattern LEVEL "0" ->
+          let (p, ty) =
+            match p with
+            | CPatCast (_, p, ty) -> (p, Some ty)
+            | _ -> (p, None)
+          in
+          [LocalPattern (!@loc, p, ty)]
     ] ]
   ;
   typeclass_constraint:
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
deleted file mode 100644
index 959b0e89..00000000
--- a/parsing/g_ltac.ml4
+++ /dev/null
@@ -1,260 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Compat
-open Constrexpr
-open Tacexpr
-open Misctypes
-open Genarg
-open Genredexpr
-open Tok (* necessary for camlp4 *)
-
-open Pcoq
-open Pcoq.Prim
-open Pcoq.Tactic
-
-let fail_default_value = ArgArg 0
-
-let arg_of_expr = function
-    TacArg (loc,a) -> a
-  | e -> Tacexp (e:raw_tactic_expr)
-
-let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
-let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
-
-(* Tactics grammar rules *)
-
-GEXTEND Gram
-  GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
-          constr_may_eval constr_eval;
-
-  tactic_then_last:
-    [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
-          Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta)
-      | -> [||]
-    ] ]
-  ;
-  tactic_then_gen:
-    [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last)
-      | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l))
-      | ".."; l = tactic_then_last -> ([], Some (TacId [], l))
-      | ta = tactic_expr -> ([ta], None)
-      | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last)
-      | -> ([TacId []], None)
-    ] ]
-  ;
-  tactic_then_locality: (* [true] for the local variant [TacThens] and [false]
-                           for [TacExtend] *)
-  [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ]
-  ;
-  tactic_expr:
-    [ "5" RIGHTA
-      [ te = binder_tactic -> te ]
-    | "4" LEFTA
-      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
-      | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1)
-      | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" ->
-	  match l , tail with
-          | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
-	  | true  , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
-          | false , None -> TacThen (ta0,TacDispatch first)
-	  | true  , None -> TacThens (ta0,first) ]
-    | "3" RIGHTA
-      [ IDENT "try"; ta = tactic_expr -> TacTry ta
-      | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
-      | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
-      | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta)
-      | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
-      | IDENT "progress"; ta = tactic_expr -> TacProgress ta
-      | IDENT "once"; ta = tactic_expr -> TacOnce ta
-      | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta
-      | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
-(*To do: put Abstract in Refiner*)
-      | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
-      | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
-          TacAbstract (tc,Some s) ]
-(*End of To do*)
-    | "2" RIGHTA
-      [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1)
-      | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) 
-      | IDENT "tryif" ; ta = tactic_expr ;
-              "then" ; tat = tactic_expr ;
-              "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae)
-      | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
-      | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
-    | "1" RIGHTA
-      [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
-          TacMatchGoal (b,false,mrl)
-      | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
-        mrl = match_context_list; "end" ->
-          TacMatchGoal (b,true,mrl)
-      |	b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
-          TacMatch (b,c,mrl)
-      | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-	  TacFirst l
-      | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-	  TacSolve l
-      | IDENT "idtac"; l = LIST0 message_token -> TacId l
-      | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ];
-	  l = LIST0 message_token -> TacFail (g,n,l)
-      | st = simple_tactic -> st
-      | IDENT "constr"; ":"; c = Constr.constr ->
-          TacArg(!@loc,ConstrMayEval(ConstrTerm c))
-      | a = tactic_top_or_arg -> TacArg(!@loc,a)
-      | r = reference; la = LIST0 tactic_arg ->
-          TacArg(!@loc,TacCall (!@loc,r,la)) ]
-    | "0"
-      [ "("; a = tactic_expr; ")" -> a
-      | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
-          begin match tail with
-          | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
-          | None -> TacDispatch tf
-          end
-      | a = tactic_atom -> TacArg (!@loc,a) ] ]
-  ;
-  failkw:
-  [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ]
-  ;
-  (* binder_tactic: level 5 of tactic_expr *)
-  binder_tactic:
-    [ RIGHTA
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
-          TacFun (it,body)
-      | "let"; isrec = [IDENT "rec" -> true | -> false];
-          llc = LIST1 let_clause SEP "with"; "in";
-          body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body)
-      | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ]
-  ;
-  (* Tactic arguments *)
-  tactic_arg:
-    [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a
-      | "ltac:"; n = natural -> TacGeneric (genarg_of_int n)
-      | a = tactic_top_or_arg -> a
-      | r = reference -> Reference r
-      | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
-      (* Unambigous entries: tolerated w/o "ltac:" modifier *)
-      | id = METAIDENT -> MetaIdArg (!@loc,true,id)
-      | "()" -> TacGeneric (genarg_of_unit ()) ] ]
-  ;
-  (* Can be used as argument and at toplevel in tactic expressions. *)
-  tactic_top_or_arg:
-    [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c
-      | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
-        TacGeneric (genarg_of_ipattern ipat)
-      | c = constr_eval -> ConstrMayEval c
-      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
-      | IDENT "type_term"; c=uconstr -> TacPretype c
-      | IDENT "numgoals" -> TacNumgoals ] ]
-  ;
-  (* If a qualid is given, use its short name. TODO: have the shortest
-     non ambiguous name where dots are replaced by "_"? Probably too
-     verbose most of the time. *)
-  fresh_id:
-    [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
-	| qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ]
-  ;
-  constr_eval:
-    [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
-          ConstrEval (rtc,c)
-      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
-          ConstrContext (id,c)
-      | IDENT "type"; IDENT "of"; c = Constr.constr ->
-          ConstrTypeOf c ] ]
-  ;
-  constr_may_eval: (* For extensions *)
-    [ [ c = constr_eval -> c
-      | c = Constr.constr -> ConstrTerm c ] ]
-  ;
-  tactic_atom:
-    [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id)
-      | n = integer -> TacGeneric (genarg_of_int n)
-      | r = reference -> TacCall (!@loc,r,[])
-      | "()" -> TacGeneric (genarg_of_unit ()) ] ]
-  ;
-  match_key:
-    [ [ "match" -> Once
-      | "lazymatch" -> Select
-      | "multimatch" -> General ] ]
-  ;
-  input_fun:
-    [ [ "_" -> None
-      | l = ident -> Some l ] ]
-  ;
-  let_clause:
-    [ [ id = identref; ":="; te = tactic_expr ->
-         (id, arg_of_expr te)
-      | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
-         (id, arg_of_expr (TacFun(args,te))) ] ]
-  ;
-  match_pattern:
-    [ [ IDENT "context";  oid = OPT Constr.ident;
-          "["; pc = Constr.lconstr_pattern; "]" ->
-        let mode = not (!Flags.tactic_context_compat) in
-        Subterm (mode, oid, pc)
-      | IDENT "appcontext";  oid = OPT Constr.ident;
-          "["; pc = Constr.lconstr_pattern; "]" ->
-        msg_warning (strbrk "appcontext is deprecated");
-        Subterm (true,oid, pc)
-      | pc = Constr.lconstr_pattern -> Term pc ] ]
-  ;
-  match_hyps:
-    [ [ na = name; ":"; mp =  match_pattern -> Hyp (na, mp)
-      | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt)
-      | na = name; ":="; mpv = match_pattern ->
-	  let t, ty =
-	    match mpv with
-	    | Term t -> (match t with
-	      | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
-	      | _ -> mpv, None)
-	    | _ -> mpv, None
-	  in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty)
-    ] ]
-  ;
-  match_context_rule:
-    [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
-        "=>"; te = tactic_expr -> Pat (largs, mp, te)
-      | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
-        "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te)
-      | "_"; "=>"; te = tactic_expr -> All te ] ]
-  ;
-  match_context_list:
-    [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
-      | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
-  ;
-  match_rule:
-    [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te)
-      | "_"; "=>"; te = tactic_expr -> All te ] ]
-  ;
-  match_list:
-    [ [ mrl = LIST1 match_rule SEP "|" -> mrl
-      | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
-  ;
-  message_token:
-    [ [ id = identref -> MsgIdent id
-      | s = STRING -> MsgString s
-      | n = integer -> MsgInt n ] ]
-  ;
-
-  ltac_def_kind:
-    [ [ ":=" -> false
-      | "::=" -> true ] ]
-  ;
-
-  (* Definitions for tactics *)
-  tacdef_body:
-    [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
-	  (name, redef, TacFun (it, body))
-      | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
-	  (name, redef, body) ] ]
-  ;
-  tactic:
-    [ [ tac = tactic_expr -> tac ] ]
-  ;
-  END
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 5297c163..b90e06cd 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -15,7 +15,7 @@ open Pcoq
 open Pcoq.Prim
 
 let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
-let _ = List.iter Lexer.add_keyword prim_kw
+let _ = List.iter CLexer.add_keyword prim_kw
 
 
 let local_make_qualid l id = make_qualid (DirPath.make l) id
@@ -28,7 +28,7 @@ let my_int_of_string loc s =
     if n > 1024 * 2048 then raise Exit;
     n
   with Failure _ | Exit ->
-    Errors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
+    CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
 
 GEXTEND Gram
   GLOBAL:
@@ -93,7 +93,7 @@ GEXTEND Gram
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then Errors.user_err_loc(!@loc, "", Pp.str"Empty string."); s
+        if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 422384f3..70c5d5d8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -88,7 +88,7 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
       | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
-      | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
+      | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id)
       | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis
       | IDENT "Guarded" -> VernacCheckGuard
       (* Hints for Auto and EAuto *)
@@ -103,10 +103,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 ] ]
@@ -116,9 +115,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)
@@ -134,6 +132,8 @@ GEXTEND Gram
       | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ]
   ;
   mode:
-    [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ]
+    [ [ l = LIST1 [ "+" -> ModeInput
+                  | "!" -> ModeNoHeadEvar
+                  | "-" -> ModeOutput ] -> l ] ]
   ;
 END
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2a00a176..3152afb2 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Tacexpr
 open Genredexpr
@@ -22,10 +22,10 @@ open Decl_kinds
 open Pcoq
 
 
-let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta]
+let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
 
 let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter Lexer.add_keyword tactic_kw
+let _ = List.iter CLexer.add_keyword tactic_kw
 
 let err () = raise Stream.Failure
 
@@ -111,8 +111,8 @@ let check_for_coloneq =
       | KEYWORD "(" -> skip_binders 2
       | _ -> err ())
 
-let lookup_at_as_coma =
-  Gram.Entry.of_parser "lookup_at_as_coma"
+let lookup_at_as_comma =
+  Gram.Entry.of_parser "lookup_at_as_comma"
     (fun strm ->
       match get_tok (stream_nth 0 strm) with
 	| KEYWORD (","|"at"|"as") -> ()
@@ -141,11 +141,11 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
   (id,CProdN(loc,bl,ty))
 
 (* Functions overloaded by quotifier *)
-let induction_arg_of_constr (c,lbind as clbind) = match lbind with
+let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
   | NoBindings ->
     begin
       try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
-      with e when Errors.noncritical e -> ElimOnConstr clbind
+      with e when CErrors.noncritical e -> ElimOnConstr clbind
     end
   | _ -> ElimOnConstr clbind
 
@@ -211,12 +211,16 @@ let merge_occurrences loc cl = function
     in
     (Some p, ans)
 
+let warn_deprecated_eqn_syntax =
+  CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated"
+         (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg))
+
 (* Auxiliary grammar rules *)
 
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
   bindings red_expr int_or_var open_constr uconstr
-  simple_intropattern clause_dft_concl hypident;
+  simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
@@ -231,16 +235,16 @@ GEXTEND Gram
     [ [ id = identref -> id ] ]
   ;
   open_constr:
-    [ [ c = constr -> ((),c) ] ]
+    [ [ c = constr -> c ] ]
   ;
   uconstr:
     [ [ c = constr -> c ] ]
   ;
-  induction_arg:
+  destruction_arg:
     [ [ n = natural -> (None,ElimOnAnonHyp n)
       | test_lpar_id_rpar; c = constr_with_bindings ->
-        (Some false,induction_arg_of_constr c)
-      | c = constr_with_bindings -> (None,induction_arg_of_constr c)
+        (Some false,destruction_arg_of_constr c)
+      | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c
     ] ]
   ;
   constr_with_bindings_arg:
@@ -281,19 +285,23 @@ GEXTEND Gram
   intropatterns:
     [ [ l = LIST0 nonsimple_intropattern -> l ]]
   ;
+  ne_intropatterns:
+    [ [ l = LIST1 nonsimple_intropattern -> l ]]
+  ;
   or_and_intropattern:
-    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> tc
-      | "()" -> [[]]
-      | "("; si = simple_intropattern; ")" -> [[si]]
+    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc
+      | "()" -> IntroAndPattern []
+      | "("; si = simple_intropattern; ")" -> IntroAndPattern [si]
       | "("; si = simple_intropattern; ",";
-             tc = LIST1 simple_intropattern SEP "," ; ")" -> [si::tc]
+             tc = LIST1 simple_intropattern SEP "," ; ")" ->
+             IntroAndPattern (si::tc)
       | "("; si = simple_intropattern; "&";
 	     tc = LIST1 simple_intropattern SEP "&" ; ")" ->
 	  (* (A & B & C) is translated into (A,(B,C)) *)
 	  let rec pairify = function
-	    | ([]|[_]|[_;_]) as l -> [l]
-	    | t::q -> [[t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (pairify q)))]]
-	  in pairify (si::tc) ] ]
+	    | ([]|[_]|[_;_]) as l -> l
+	    | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+	  in IntroAndPattern (pairify (si::tc)) ] ]
   ;
   equality_intropattern:
     [ [ "->" -> IntroRewrite true
@@ -334,20 +342,20 @@ GEXTEND Gram
           ExplicitBindings bl
       | bl = LIST1 constr -> ImplicitBindings bl ] ]
   ;
-  opt_bindings:
-    [ [ bl = LIST1 bindings SEP "," -> bl | -> [NoBindings] ] ]
-  ;
   constr_with_bindings:
     [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
   with_bindings:
     [ [ "with"; bl = bindings -> bl | -> NoBindings ] ]
   ;
-  red_flag:
-    [ [ IDENT "beta" -> FBeta
-      | IDENT "iota" -> FIota
-      | IDENT "zeta" -> FZeta
-      | IDENT "delta"; d = delta_flag -> d
+  red_flags:
+    [ [ IDENT "beta" -> [FBeta]
+      | IDENT "iota" -> [FMatch;FFix;FCofix]
+      | IDENT "match" -> [FMatch]
+      | IDENT "fix" -> [FFix]
+      | IDENT "cofix" -> [FCofix]
+      | IDENT "zeta" -> [FZeta]
+      | IDENT "delta"; d = delta_flag -> [d]
     ] ]
   ;
   delta_flag:
@@ -357,7 +365,7 @@ GEXTEND Gram
     ] ]
   ;
   strategy_flag:
-    [ [ s = LIST1 red_flag -> Redops.make_red_flag s
+    [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s)
       | d = delta_flag -> all_with d
     ] ]
   ;
@@ -450,15 +458,6 @@ GEXTEND Gram
     [ [ check_for_coloneq; "(";  id = ident; bl = LIST0 simple_binder;
         ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
   ;
-  hintbases:
-    [ [ "with"; "*" -> None
-      | "with"; l = LIST1 [ x = IDENT -> x] -> Some l
-      | -> Some [] ] ]
-  ;
-  auto_using:
-    [ [ "using"; l = LIST1 constr SEP "," -> l
-      | -> [] ] ]
-  ;
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
@@ -477,42 +476,35 @@ GEXTEND Gram
   eqn_ipat:
     [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
       | IDENT "_eqn"; ":"; pat = naming_intropattern ->
-        let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in
-        msg_warning (strbrk msg); Some (!@loc, pat)
+         let loc = !@loc in
+	 warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat)
       | IDENT "_eqn" ->
-        let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in
-        msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
+         let loc = !@loc in
+	 warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous)
       | -> None ] ]
   ;
   as_name:
     [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
   ;
   by_tactic:
-    [ [ "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
-      | -> TacId [] ] ]
-  ;
-  opt_by_tactic:
     [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
     | -> None ] ]
   ;
-  rename :
-    [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
-  ;
   rewriter :
-    [ [ "!"; c = constr_with_bindings -> (RepeatPlus,(None,c))
+    [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c)
       | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
-      | n = natural; "!"; c = constr_with_bindings -> (Precisely n,(None,c))
+      | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c)
       |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
       | n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
-      | c = constr_with_bindings -> (Precisely 1, (None,c))
+      | c = constr_with_bindings_arg -> (Precisely 1, c)
       ] ]
   ;
   oriented_rewriter :
     [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
   ;
   induction_clause:
-    [ [ c = induction_arg; pat = as_or_and_ipat; eq = eqn_ipat; cl = opt_clause
-        -> (c,(eq,pat),cl) ] ]
+    [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
+        cl = opt_clause -> (c,(eq,pat),cl) ] ]
   ;
   induction_clause_list:
     [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator;
@@ -523,23 +515,15 @@ GEXTEND Gram
         | _,_,Some _ -> err ()
         | _,_,None -> (ic,el) ]]
   ;
-  move_location:
-    [ [ IDENT "after"; id = id_or_meta -> MoveAfter id
-      | IDENT "before"; id = id_or_meta -> MoveBefore id
-      | "at"; IDENT "top" -> MoveFirst
-      | "at"; IDENT "bottom" -> MoveLast ] ]
-  ;
   simple_tactic:
     [ [
       (* Basic tactics *)
-        IDENT "intros"; pl = intropatterns -> TacAtom (!@loc, TacIntroPattern pl)
-      | IDENT "intro"; id = ident; hto = move_location ->
-	  TacAtom (!@loc, TacIntroMove (Some id, hto))
-      | IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto))
-      | IDENT "intro"; id = ident -> TacAtom (!@loc, TacIntroMove (Some id, MoveLast))
-      | IDENT "intro" -> TacAtom (!@loc, TacIntroMove (None, MoveLast))
-
-      | IDENT "exact"; c = constr -> TacAtom (!@loc, TacExact c)
+        IDENT "intros"; pl = ne_intropatterns ->
+          TacAtom (!@loc, TacIntroPattern (false,pl))
+      | IDENT "intros" ->
+          TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false]))
+      | IDENT "eintros"; pl = ne_intropatterns ->
+          TacAtom (!@loc, TacIntroPattern (true,pl))
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
@@ -557,12 +541,8 @@ GEXTEND Gram
           TacAtom (!@loc, TacElim (true,cl,el))
       | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl)
       | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
-      | "fix"; n = natural -> TacAtom (!@loc, TacFix (None,n))
-      | "fix"; id = ident; n = natural -> TacAtom (!@loc, TacFix (Some id,n))
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
 	  TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd))
-      | "cofix" -> TacAtom (!@loc, TacCofix None)
-      | "cofix"; id = ident -> TacAtom (!@loc, TacCofix (Some id))
       | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
 	  TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd))
 
@@ -605,60 +585,26 @@ GEXTEND Gram
       | IDENT "generalize"; c = constr; l = LIST1 constr ->
 	  let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
           TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l)))
-      | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs;
+      | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
           na = as_name;
           l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
           TacAtom (!@loc, TacGeneralize (((nl,c),na)::l))
-      | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c)
 
       (* Derived basic tactics *)
       | IDENT "induction"; ic = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct (true,false,ic))
       | IDENT "einduction"; ic = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(true,true,ic))
-      | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
-	  h2 = quantified_hypothesis -> TacAtom (!@loc, TacDoubleInduction (h1,h2))
       | IDENT "destruct"; icl = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(false,false,icl))
       | IDENT "edestruct";  icl = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
-      (* Automation tactic *)
-      | IDENT "trivial"; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacTrivial (Off, lems, db))
-      | IDENT "info_trivial"; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacTrivial (Info, lems, db))
-      | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacTrivial (Debug, lems, db))
-      | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacAuto (Off, n, lems, db))
-      | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacAuto (Info, n, lems, db))
-      | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacAuto (Debug, n, lems, db))
-
-      (* Context management *)
-      | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
-      | IDENT "clear"; l = LIST0 id_or_meta ->
-        let is_empty = match l with [] -> true | _ -> false in
-        TacAtom (!@loc, TacClear (is_empty, l))
-      | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l)
-      | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
-	  TacAtom (!@loc, TacMove (hfrom,hto))
-      | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
-
-      (* Constructors *)
-      | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll))
-      | IDENT "eexists"; bll = opt_bindings ->
-	  TacAtom (!@loc, TacSplit (true,bll))
-      (* Equivalence relations *)
-      | IDENT "symmetry"; "in"; cl = in_clause -> TacAtom (!@loc, TacSymmetry cl)
-
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
+	  cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
       | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
+	  cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 839f768b..e61be53a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -8,7 +8,7 @@
 
 open Pp
 open Compat
-open Errors
+open CErrors
 open Util
 open Names
 open Constrexpr
@@ -20,22 +20,19 @@ open Misctypes
 open Tok (* necessary for camlp4 *)
 
 open Pcoq
-open Pcoq.Tactic
 open Pcoq.Prim
 open Pcoq.Constr
 open Pcoq.Vernac_
 open Pcoq.Module
 
 let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
-let _ = List.iter Lexer.add_keyword vernac_kw
+let _ = List.iter CLexer.add_keyword vernac_kw
 
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
 let query_command = Gram.entry_create "vernac:query_command"
 
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
-let noedit_mode = Gram.entry_create "vernac:noedit_command"
 let subprf = Gram.entry_create "vernac:subprf"
 
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -48,21 +45,6 @@ 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 command_entry = ref noedit_mode
-let set_command_entry e = command_entry := e
-let get_command_entry () = !command_entry
-
-
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
-    proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let set_tactic_mode () = set_command_entry tactic_mode
-let set_noedit_mode () = set_command_entry noedit_mode
-let _ = Proof_global.register_proof_mode {Proof_global.
-					    name = "Classic" ;
-					    set = set_tactic_mode ;
-					    reset = set_noedit_mode
-					 }
-
 let make_bullet s =
   let n = String.length s in
   match s.[0] with
@@ -71,26 +53,11 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
-(* Hack to parse "[ id" without dropping [ *)
-let test_bracket_ident =
-  Gram.Entry.of_parser "test_bracket_ident"
-    (fun strm ->
-      match get_tok (stream_nth 0 strm) with
-        | KEYWORD "[" ->
-            (match get_tok (stream_nth 1 strm) with
-              | IDENT _ -> ()
-	      | _ -> raise Stream.Failure)
-	| _ -> raise Stream.Failure)
-
-let default_command_entry =
-  Gram.Entry.of_parser "command_entry"
-    (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
-
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
+  GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
   vernac: FIRST
-    [ [ IDENT "Time"; l = vernac_list -> VernacTime l
-      | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l)
+    [ [ IDENT "Time"; c = located_vernac -> VernacTime c
+      | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac -> VernacFail v
 
@@ -128,28 +95,13 @@ GEXTEND Gram
       | c = subprf -> c
     ] ]
   ;
-  vernac_list:
-    [ [ c = located_vernac -> [c] ] ]
-  ;
   vernac_aux: LAST
-    [ [ prfcom = default_command_entry -> prfcom ] ]
+    [ [ prfcom = command_entry -> prfcom ] ]
   ;
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
   ;
 
-  selector:
-    [ [ n=natural; ":" -> SelectNth n
-      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
-      | IDENT "all" ; ":" -> SelectAll
-      | IDENT "par" ; ":" -> SelectAllParallel ] ]
-  ;
-
-  tactic_mode:
-  [ [ gln = OPT selector;
-      tac = subgoal_command -> tac gln ] ]
-  ;
-
   subprf:
   [ [ s = BULLET -> VernacBullet (make_bullet s)
     | "{" -> VernacSubproof None
@@ -164,35 +116,37 @@ GEXTEND Gram
                     | None -> c None
                     | _ ->
                         VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
-                  end
-      | info = OPT [IDENT "Info";n=natural -> n];
-        tac = Tactic.tactic;
-        use_dft_tac = [ "." -> false | "..." -> true ] ->
-        (fun g ->
-            let g = Option.default (Proof_global.get_default_goal_selector ()) g in
-            VernacSolve(g,info,tac,use_dft_tac)) ] ]
+                  end ] ]
   ;
   located_vernac:
     [ [ v = vernac -> !@loc, v ] ]
   ;
 END
 
-let test_plurial_form = function
+let warn_plural_command =
+  CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled
+         (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd))
+
+let test_plural_form loc kwd = function
   | [(_,([_],_))] ->
-      Flags.if_verbose msg_warning
-   (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
+     warn_plural_command ~loc:!@loc kwd
   | _ -> ()
 
-let test_plurial_form_types = function
+let test_plural_form_types loc kwd = function
   | [([_],_)] ->
-      Flags.if_verbose msg_warning
-   (strbrk "Keywords Implicit Types expect more than one type")
+     warn_plural_command ~loc:!@loc kwd
   | _ -> ()
 
+let fresh_var env c =
+  Namegen.next_ident_away (Id.of_string "pat")
+    (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c))
+
+let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var
+
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    record_field decl_notation rec_definition;
+    record_field decl_notation rec_definition pidentref;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -203,8 +157,8 @@ GEXTEND Gram
           VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
-      | stre = assumptions_token; nl = inline; bl = assum_list ->
-	  test_plurial_form bl;
+      | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
+	  test_plural_form loc kwd bl;
 	  VernacAssumption (stre, nl, bl)
       | d = def_token; id = pidentref; b = def_body ->
           VernacDefinition (d, id, b)
@@ -257,11 +211,11 @@ GEXTEND Gram
       | IDENT "Conjecture" -> (None, Conjectural) ] ]
   ;
   assumptions_token:
-    [ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
-      | IDENT "Variables" -> (Some Discharge, Definitional)
-      | IDENT "Axioms" -> (None, Logical)
-      | IDENT "Parameters" -> (None, Definitional)
-      | IDENT "Conjectures" -> (None, Conjectural) ] ]
+    [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical))
+      | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional))
+      | IDENT "Axioms" -> ("Axioms", (None, Logical))
+      | IDENT "Parameters" -> ("Parameters", (None, Definitional))
+      | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
@@ -272,8 +226,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)
@@ -289,11 +243,19 @@ GEXTEND Gram
   (* Simple definitions *)
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
+      let (bl, c) = expand_pattern_binders mkCLambdaN bl c in
       (match c with
           CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
-	DefineBody (bl, red, c, Some t)
+        let ((bl, c), tyo) =
+          if List.exists (function LocalPattern _ -> true | _ -> false) bl
+          then
+            let c = CCast (!@loc, c, CastConv t) in
+            (expand_pattern_binders mkCLambdaN bl c, None)
+          else ((bl, c), Some t)
+        in
+	DefineBody (bl, red, c, tyo)
     | bl = binders; ":"; t = lconstr ->
         ProveBody (bl, t) ] ]
   ;
@@ -462,6 +424,10 @@ let starredidentreflist_to_expr l =
   | [] -> SsEmpty
   | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
 
+let warn_deprecated_include_type =
+  CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated"
+         (fun () -> strbrk "Include Type is deprecated; use Include instead")
+
 (* Modules and Sections *)
 GEXTEND Gram
   GLOBAL: gallina_ext module_expr module_type section_subset_expr;
@@ -501,9 +467,8 @@ GEXTEND Gram
       | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
 	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
-	  Flags.if_verbose
-            msg_warning (strbrk "Include Type is deprecated; use Include instead");
-          VernacInclude(e::l) ] ]
+	 warn_deprecated_include_type ~loc:!@loc ();
+	 VernacInclude(e::l) ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> Some false
@@ -607,9 +572,23 @@ GEXTEND Gram
   ;
 END
 
+let warn_deprecated_arguments_scope =
+  CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated"
+         (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead")
+
+let warn_deprecated_implicit_arguments =
+  CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated"
+         (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead")
+
+let warn_deprecated_arguments_syntax =
+  CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated"
+         (fun () -> strbrk "The \"/\" and \"!\" modifiers have an effect only "
+                    ++ strbrk "in the first arguments list. The syntax allowing"
+                    ++ strbrk " them to appear in other lists is deprecated.")
+
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
-  GLOBAL: gallina_ext instance_name;
+  GLOBAL: gallina_ext instance_name hint_info;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -662,81 +641,69 @@ 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
 
       (* Arguments *)
       | IDENT "Arguments"; qid = smart_global; 
-        impl = LIST1 [ l = LIST0
-        [ item = argument_spec ->
-            let id, r, s = item in [`Id (id,r,s,false,false)]
-        | "/" -> [`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
-        | "["; 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
-        | "{"; 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
-        ] -> l ] SEP ",";
+        args = LIST0 argument_spec_block;
+        more_implicits = OPT
+          [ ","; impl = LIST1
+            [ impl = LIST0 more_implicits_block ->
+              let warn_deprecated = List.exists fst impl in
+              if warn_deprecated then warn_deprecated_arguments_syntax ~loc:!@loc ();
+              List.flatten (List.map snd impl)]
+            SEP "," -> impl
+          ];
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
          let mods = match mods with None -> [] | Some l -> List.flatten l in
-         let impl = List.map List.flatten impl in
-         let rec aux n (narg, impl) = function
-           | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl
-           | `Slash :: tl -> aux (n+1) (n, impl) tl
-           | [] -> narg, impl in
-         let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in
-         let nargs, rest = List.hd nargs, List.tl nargs in
-         if List.exists (fun arg -> not (Int.equal arg nargs)) rest then
-           error "All arguments lists must have the same length";
-         let err_incompat x y =
-           error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
-         if nargs > 0 && List.mem `ReductionNeverUnfold mods then
-           err_incompat "simpl never" "/";
-         if List.mem `ReductionNeverUnfold mods &&
-            List.mem `ReductionDontExposeCase mods then
-           err_incompat "simpl never" "simpl nomatch";
-         VernacArguments (qid, impl, nargs, mods)
-
+         let slash_position = ref None in
+         let rec parse_args i = function
+           | [] -> []
+           | `Id x :: args -> x :: parse_args (i+1) args
+           | `Slash :: args ->
+              if Option.is_empty !slash_position then
+                (slash_position := Some i; parse_args i args)
+              else
+                error "The \"/\" modifier can occur only once"
+         in
+         let args = parse_args 0 (List.flatten args) in
+         let more_implicits = Option.default [] more_implicits in
+         VernacArguments (qid, args, more_implicits, !slash_position, mods)
+
+ 
      (* moved there so that camlp5 factors it with the previous rule *)
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
-        msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
+	warn_deprecated_arguments_scope ~loc:!@loc ();
         VernacArgumentsScope (qid,scl)
 
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
 	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
-	   Flags.if_verbose
-             msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
-	   VernacDeclareImplicits (qid,pos)
+	 warn_deprecated_implicit_arguments ~loc:!@loc ();
+	 VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
 	   VernacReserve bl
 
       | IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
-          test_plurial_form_types bl;
+          test_plural_form_types loc "Implicit Types" bl;
            VernacReserve bl
 
       | IDENT "Generalizable"; 
@@ -775,6 +742,55 @@ GEXTEND Gram
        snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s
     ]
   ];
+  (* List of arguments implicit status, scope, modifiers *)
+  argument_spec_block: [
+    [ item = argument_spec ->
+      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 (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 (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 (name,recarg_like,notation_scope) ->
+           `Id { name=name; recarg_like=recarg_like;
+                 notation_scope=f notation_scope;
+                 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: [
+    [ (bang,name) = name_or_bang -> (bang, [(snd name, Vernacexpr.NotImplicit)])
+    | "/" -> (true (* Should warn about deprecated syntax *), [])
+    | "["; items = LIST1 name_or_bang; "]" ->
+       (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.Implicit)) items)
+    | "{"; items = LIST1 name_or_bang; "}" ->
+       (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.MaximallyImplicit)) items)
+    ]
+  ];
   strategy_level:
     [ [ IDENT "expand" -> Conv_oracle.Expand
       | IDENT "opaque" -> Conv_oracle.Opaque
@@ -783,10 +799,15 @@ GEXTEND Gram
       | IDENT "transparent" -> Conv_oracle.transparent ] ]
   ;
   instance_name:
-    [ [ name = identref; sup = OPT binders ->
-	  (let (loc,id) = name in (loc, Name id)),
+    [ [ name = pidentref; sup = OPT binders ->
+	  (let ((loc,id),l) = name in ((loc, Name id),l)),
           (Option.default [] sup)
-      | -> (!@loc, Anonymous), []  ] ]
+      | -> ((!@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] ] ]
@@ -804,17 +825,13 @@ GEXTEND Gram
   GLOBAL: command query_command class_rawexpr;
 
   command:
-    [ [ IDENT "Ltac";
-        l = LIST1 tacdef_body SEP "with" ->
-          VernacDeclareTacticDefinition (true, l)
-
-      | IDENT "Comments"; l = LIST0 comment -> VernacComments l
+    [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
 
       (* 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
@@ -870,7 +887,20 @@ GEXTEND Gram
 
       (* For acting on parameter tables *)
       | "Set"; table = option_table; v = option_value ->
-  	  VernacSetOption (table,v)
+        begin match v with
+        | StringValue 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
+            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 ->
   	  VernacSetOption (table,BoolValue true)
       | IDENT "Unset"; table = option_table ->
@@ -943,7 +973,6 @@ GEXTEND Gram
       | IDENT "Classes" ->  PrintClasses
       | IDENT "TypeClasses" -> PrintTypeClasses
       | IDENT "Instances"; qid = smart_global -> PrintInstances qid
-      | IDENT "Ltac"; qid = global -> PrintLtac qid
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
@@ -954,7 +983,6 @@ GEXTEND Gram
       | IDENT "Hint"; qid = smart_global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
-      | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s
@@ -1083,7 +1111,7 @@ GEXTEND Gram
 	 VernacDelimiters (sc, None)
 
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
-       refl = LIST1 smart_global -> VernacBindScope (sc,refl)
+       refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
      | IDENT "Infix"; local = obsolete_locality;
 	 op = ne_lstring; ":="; p = constr;
@@ -1102,10 +1130,6 @@ GEXTEND Gram
      | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
            VernacNotationAddFormat (n,s,fmt)
 
-     | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
-	 pil = LIST1 production_item; ":="; t = Tactic.tactic
-         -> VernacTacticNotation (n,pil,t)
-
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   Metasyntax.check_infix_modifiers l;
@@ -1131,9 +1155,6 @@ GEXTEND Gram
   obsolete_locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
-  tactic_level:
-    [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
-  ;
   level:
     [ [ IDENT "level"; n = natural -> NumLevel n
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
@@ -1143,10 +1164,10 @@ GEXTEND Gram
       | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc NonA
-      | IDENT "only"; IDENT "parsing" ->
-        SetOnlyParsing Flags.Current
+      | IDENT "only"; IDENT "printing" -> SetOnlyPrinting
+      | 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
@@ -1165,10 +1186,4 @@ GEXTEND Gram
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
-  production_item:
-    [ [ s = ne_string -> TacTerm s
-      | nt = IDENT;
-        po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
-                   ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ]
-  ;
 END
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 13ed8046..8df519b5 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -3,5 +3,3 @@ G_vernac
 G_prim
 G_proofs
 G_tactic
-G_ltac
-G_obligations
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index a0cb8319..0e1c79c9 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,6 @@
 Tok
 Compat
-Lexer
+CLexer
 Pcoq
 Egramml
 Egramcoq
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
new file mode 100644
index 00000000..7dc02190
--- /dev/null
+++ b/parsing/pcoq.ml
@@ -0,0 +1,527 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Compat
+open CErrors
+open Util
+open Extend
+open Genarg
+
+(** The parser of Coq *)
+
+module G = GrammarMake (CLexer)
+
+let warning_verbose = Compat.warning_verbose
+
+let of_coq_assoc = function
+| Extend.RightA -> CompatGramext.RightA
+| Extend.LeftA -> CompatGramext.LeftA
+| Extend.NonA -> CompatGramext.NonA
+
+let of_coq_position = function
+| Extend.First -> CompatGramext.First
+| Extend.Last -> CompatGramext.Last
+| Extend.Before s -> CompatGramext.Before s
+| Extend.After s -> CompatGramext.After s
+| Extend.Level s -> CompatGramext.Level s
+
+module Symbols = GramextMake(G)
+
+let camlp4_verbosity silent f x =
+  let a = !warning_verbose in
+  warning_verbose := silent;
+  f x;
+  warning_verbose := a
+
+let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
+
+(** Grammar extensions *)
+
+(** NB: [extend_statment =
+         gram_position option * single_extend_statment list]
+    and [single_extend_statment =
+         string option * gram_assoc option * production_rule list]
+    and [production_rule = symbol list * action]
+
+    In [single_extend_statement], first two parameters are name and
+    assoc iff a level is created *)
+
+(** Binding general entry keys to symbol *)
+
+let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function
+| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc))
+| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x))
+
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
+  | Atoken t -> Symbols.stoken t
+  | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
+  | Alist1sep (s,sep) ->
+      Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
+  | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
+  | Alist0sep (s,sep) ->
+      Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
+  | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
+  | Aself -> Symbols.sself
+  | Anext -> Symbols.snext
+  | Aentry e ->
+    Symbols.snterm (G.Entry.obj e)
+  | Aentryl (e, n) ->
+    Symbols.snterml (G.Entry.obj e, string_of_int n)
+  | Arules rs ->
+    G.srules' (List.map symbol_of_rules rs)
+
+and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
+| Stop -> fun accu -> accu
+| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
+
+and symbol_of_rules : type a. a Extend.rules -> _ = function
+| Rules (r, act) ->
+  let symb = symbol_of_rule r.norec_rule [] in
+  let act = of_coq_action r.norec_rule act in
+  (symb, act)
+
+let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
+| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
+
+let of_coq_single_extend_statement (lvl, assoc, rule) =
+  (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
+
+let of_coq_extend_statement (pos, st) =
+  (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
+
+(** Type of reinitialization data *)
+type gram_reinit = gram_assoc * gram_position
+
+type extend_rule =
+| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule
+
+type ext_kind =
+  | ByGrammar of extend_rule
+  | ByEXTEND of (unit -> unit) * (unit -> unit)
+
+(** The list of extensions *)
+
+let camlp4_state = ref []
+
+(** Deletion *)
+
+let grammar_delete e reinit (pos,rls) =
+  List.iter
+    (fun (n,ass,lev) ->
+      List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+    (List.rev rls);
+  match reinit with
+  | Some (a,ext) ->
+    let a = of_coq_assoc a in
+    let ext = of_coq_position ext in
+    let lev = match pos with
+    | Some (CompatGramext.Level n) -> n
+    | _ -> assert false
+    in
+    maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]])
+  | None -> ()
+
+(** Extension *)
+
+let grammar_extend e reinit ext =
+  let ext = of_coq_extend_statement ext in
+  let undo () = grammar_delete e reinit ext in
+  let redo () = camlp4_verbosity false (maybe_uncurry (G.extend e)) ext in
+  camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state;
+  redo ()
+
+let grammar_extend_sync e reinit ext =
+  camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
+  camlp4_verbosity false (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext)
+
+(** The apparent parser of Coq; encapsulate G to keep track
+    of the extensions. *)
+
+module Gram =
+  struct
+    include G
+    let extend e =
+      maybe_curry
+	(fun ext ->
+	   camlp4_state :=
+	     (ByEXTEND ((fun () -> grammar_delete e None ext),
+			(fun () -> maybe_uncurry (G.extend e) ext)))
+	   :: !camlp4_state;
+	   maybe_uncurry (G.extend e) ext)
+    let delete_rule e pil =
+      (* spiwack: if you use load an ML module which contains GDELETE_RULE
+	  in a section, God kills a kitty. As it would corrupt remove_grammars.
+          There does not seem to be a good way to undo a delete rule. As deleting
+	  takes fewer arguments than extending. The production rule isn't returned
+	  by delete_rule. If we could retrieve the necessary information, then
+	  ByEXTEND provides just the framework we need to allow this in section.
+	  I'm not entirely sure it makes sense, but at least it would be more correct.
+          *)
+      G.delete_rule e pil
+  end
+
+(** Remove extensions
+
+   [n] is the number of extended entries (not the number of Grammar commands!)
+   to remove. *)
+
+let rec remove_grammars n =
+  if n>0 then
+    (match !camlp4_state with
+       | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove")
+       | ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
+           grammar_delete g reinit (of_coq_extend_statement ext);
+           camlp4_state := t;
+           remove_grammars (n-1)
+       | ByEXTEND (undo,redo)::t ->
+           undo();
+           camlp4_state := t;
+           remove_grammars n;
+           redo();
+           camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
+
+let make_rule r = [None, None, r]
+
+(** An entry that checks we reached the end of the input. *)
+
+let eoi_entry en =
+  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
+  let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
+  let act = Gram.action (fun _ x loc -> x) in
+  maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+  e
+
+let map_entry f en =
+  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
+  let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
+  let act = Gram.action (fun x loc -> f x) in
+  maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+  e
+
+(* Parse a string, does NOT check if the entire string was read
+   (use eoi_entry) *)
+
+let parse_string f x =
+  let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
+
+type gram_universe = string
+
+let utables : (string, unit) Hashtbl.t =
+  Hashtbl.create 97
+
+let create_universe u =
+  let () = Hashtbl.add utables u () in
+  u
+
+let uprim   = create_universe "prim"
+let uconstr = create_universe "constr"
+let utactic = create_universe "tactic"
+let uvernac = create_universe "vernac"
+
+let get_univ u =
+  if Hashtbl.mem utables u then u
+  else raise Not_found
+
+let new_entry u s =
+  let ename = u ^ ":" ^ s in
+  let e = Gram.entry_create ename in
+  e
+
+let make_gen_entry u s = new_entry u s
+
+module GrammarObj =
+struct
+  type ('r, _, _) obj = 'r Gram.entry
+  let name = "grammar"
+  let default _ = None
+end
+
+module Grammar = Register(GrammarObj)
+
+let register_grammar = Grammar.register0
+let genarg_grammar = Grammar.obj
+
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
+  let e = new_entry u s in
+  let Rawwit t = etyp in
+  let () = Grammar.register0 t e in
+  e
+
+(* Initial grammar entries *)
+
+module Prim =
+  struct
+    let gec_gen n = make_gen_entry uprim n
+
+    (* Entries that can be referred via the string -> Gram.entry table *)
+    (* Typically for tactic or vernac extensions *)
+    let preident = gec_gen "preident"
+    let ident = gec_gen "ident"
+    let natural = gec_gen "natural"
+    let integer = gec_gen "integer"
+    let bigint = Gram.entry_create "Prim.bigint"
+    let string = gec_gen "string"
+    let reference = make_gen_entry uprim "reference"
+    let by_notation = Gram.entry_create "by_notation"
+    let smart_global = Gram.entry_create "smart_global"
+
+    (* parsed like ident but interpreted as a term *)
+    let var = gec_gen "var"
+
+    let name = Gram.entry_create "Prim.name"
+    let identref = Gram.entry_create "Prim.identref"
+    let pidentref = Gram.entry_create "Prim.pidentref"
+    let pattern_ident = Gram.entry_create "pattern_ident"
+    let pattern_identref = Gram.entry_create "pattern_identref"
+
+    (* A synonym of ident - maybe ident will be located one day *)
+    let base_ident = Gram.entry_create "Prim.base_ident"
+
+    let qualid = Gram.entry_create "Prim.qualid"
+    let fullyqualid = Gram.entry_create "Prim.fullyqualid"
+    let dirpath = Gram.entry_create "Prim.dirpath"
+
+    let ne_string = Gram.entry_create "Prim.ne_string"
+    let ne_lstring = Gram.entry_create "Prim.ne_lstring"
+
+  end
+
+module Constr =
+  struct
+    let gec_constr = make_gen_entry uconstr
+
+    (* Entries that can be referred via the string -> Gram.entry table *)
+    let constr = gec_constr "constr"
+    let operconstr = gec_constr "operconstr"
+    let constr_eoi = eoi_entry constr
+    let lconstr = gec_constr "lconstr"
+    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"
+    let lconstr_pattern = gec_constr "lconstr_pattern"
+    let closed_binder = Gram.entry_create "constr:closed_binder"
+    let binder = Gram.entry_create "constr:binder"
+    let binders = Gram.entry_create "constr:binders"
+    let open_binders = Gram.entry_create "constr:open_binders"
+    let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
+    let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
+    let record_declaration = Gram.entry_create "constr:record_declaration"
+    let appl_arg = Gram.entry_create "constr:appl_arg"
+  end
+
+module Module =
+  struct
+    let module_expr = Gram.entry_create "module_expr"
+    let module_type = Gram.entry_create "module_type"
+  end
+
+module Tactic =
+  struct
+    (* Main entry for extensions *)
+    let simple_tactic = Gram.entry_create "tactic:simple_tactic"
+
+    (* Entries that can be referred via the string -> Gram.entry table *)
+    (* Typically for tactic user extensions *)
+    let open_constr =
+      make_gen_entry utactic "open_constr"
+    let constr_with_bindings =
+      make_gen_entry utactic "constr_with_bindings"
+    let bindings =
+      make_gen_entry utactic "bindings"
+    let hypident = Gram.entry_create "hypident"
+    let constr_may_eval = make_gen_entry utactic "constr_may_eval"
+    let constr_eval = make_gen_entry utactic "constr_eval"
+    let uconstr =
+      make_gen_entry utactic "uconstr"
+    let quantified_hypothesis =
+      make_gen_entry utactic "quantified_hypothesis"
+    let destruction_arg = make_gen_entry utactic "destruction_arg"
+    let int_or_var = make_gen_entry utactic "int_or_var"
+    let red_expr = make_gen_entry utactic "red_expr"
+    let simple_intropattern =
+      make_gen_entry utactic "simple_intropattern"
+    let in_clause = make_gen_entry utactic "in_clause"
+    let clause_dft_concl = 
+      make_gen_entry utactic "clause"
+
+
+    (* Main entries for ltac *)
+    let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+    let tactic_expr = make_gen_entry utactic "tactic_expr"
+    let binder_tactic = make_gen_entry utactic "binder_tactic"
+
+    let tactic = make_gen_entry utactic "tactic"
+
+    (* Main entry for quotations *)
+    let tactic_eoi = eoi_entry tactic
+
+  end
+
+module Vernac_ =
+  struct
+    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
+
+    (* The different kinds of vernacular commands *)
+    let gallina = gec_vernac "gallina"
+    let gallina_ext = gec_vernac "gallina_ext"
+    let command = gec_vernac "command"
+    let syntax = gec_vernac "syntax_command"
+    let vernac = gec_vernac "Vernac.vernac"
+    let vernac_eoi = eoi_entry vernac
+    let rec_definition = gec_vernac "Vernac.rec_definition"
+    let hint_info = gec_vernac "hint_info"
+    (* Main vernac entry *)
+    let main_entry = Gram.entry_create "vernac"
+    let noedit_mode = gec_vernac "noedit_command"
+
+    let () =
+      let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in
+      let act_eoi = Gram.action (fun _ loc -> None) in
+      let rule = [
+        ([ Symbols.stoken Tok.EOI ], act_eoi);
+        ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac );
+      ] in
+      maybe_uncurry (Gram.extend main_entry) (None, make_rule rule)
+
+    let command_entry_ref = ref noedit_mode
+    let command_entry =
+      Gram.Entry.of_parser "command_entry"
+        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+
+  end
+
+let main_entry = Vernac_.main_entry
+
+let set_command_entry e = Vernac_.command_entry_ref := e
+let get_command_entry () = !Vernac_.command_entry_ref
+
+let epsilon_value f e =
+  let r = Rule (Next (Stop, e), fun x _ -> f x) in
+  let ext = of_coq_extend_statement (None, [None, None, [r]]) in
+  let entry = G.entry_create "epsilon" in
+  let () = maybe_uncurry (G.extend entry) ext in
+  try Some (parse_string entry "") with _ -> None
+
+(** Synchronized grammar extensions *)
+
+module GramState = Store.Make(struct end)
+
+type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
+
+module GrammarCommand = Dyn.Make(struct end)
+module GrammarInterp = struct type 'a t = 'a grammar_extension end
+module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
+
+let grammar_interp = ref GrammarInterpMap.empty
+
+let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref []
+
+type 'a grammar_command = 'a GrammarCommand.tag
+
+let create_grammar_command name interp : _ grammar_command =
+  let obj = GrammarCommand.create name in
+  let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
+  obj
+
+let extend_grammar_command tag g =
+  let modify = GrammarInterpMap.find tag !grammar_interp in
+  let grammar_state = match !grammar_stack with
+  | [] -> GramState.empty
+  | (_, _, st) :: _ -> st
+  in
+  let (rules, st) = modify g grammar_state in
+  let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in
+  let () = List.iter iter rules in
+  let nb = List.length rules in
+  grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack
+
+let recover_grammar_command (type a) (tag : a grammar_command) : a list =
+  let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) ->
+    match GrammarCommand.eq tag tag' with
+    | None -> None
+    | Some Refl -> Some v
+  in
+  List.map_filter filter !grammar_stack
+
+let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g
+
+(* Summary functions: the state of the lexer is included in that of the parser.
+   Because the grammar affects the set of keywords when adding or removing
+   grammar rules. *)
+type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t
+
+let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ())
+
+(* We compare the current state of the grammar and the state to unfreeze,
+   by computing the longest common suffixes *)
+let factorize_grams l1 l2 =
+  if l1 == l2 then ([], [], l1) else List.share_tails l1 l2
+
+let number_of_entries gcl =
+  List.fold_left (fun n (p,_,_) -> n + p) 0 gcl
+
+let unfreeze (grams, lex) =
+  let (undo, redo, common) = factorize_grams !grammar_stack grams in
+  let n = number_of_entries undo in
+  remove_grammars n;
+  grammar_stack := common;
+  CLexer.unfreeze lex;
+  List.iter extend_dyn_grammar (List.rev_map pi2 redo)
+
+(** No need to provide an init function : the grammar state is
+    statically available, and already empty initially, while
+    the lexer state should not be resetted, since it contains
+    keywords declared in g_*.ml4 *)
+
+let _ =
+  Summary.declare_summary "GRAMMAR_LEXER"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = Summary.nop }
+
+let with_grammar_rule_protection f x =
+  let fs = freeze false in
+  try let a = f x in unfreeze fs; a
+  with reraise ->
+    let reraise = CErrors.push reraise in
+    let () = unfreeze fs in
+    iraise reraise
+
+(** Registering grammar of generic arguments *)
+
+let () =
+  let open Stdarg in
+  let open Constrarg in
+(*   Grammar.register0 wit_unit; *)
+(*   Grammar.register0 wit_bool; *)
+  Grammar.register0 wit_int (Prim.integer);
+  Grammar.register0 wit_string (Prim.string);
+  Grammar.register0 wit_pre_ident (Prim.preident);
+  Grammar.register0 wit_int_or_var (Tactic.int_or_var);
+  Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern);
+  Grammar.register0 wit_ident (Prim.ident);
+  Grammar.register0 wit_var (Prim.var);
+  Grammar.register0 wit_ref (Prim.reference);
+  Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis);
+  Grammar.register0 wit_constr (Constr.constr);
+  Grammar.register0 wit_uconstr (Tactic.uconstr);
+  Grammar.register0 wit_open_constr (Tactic.open_constr);
+  Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings);
+  Grammar.register0 wit_bindings (Tactic.bindings);
+(*   Grammar.register0 wit_hyp_location_flag; *)
+  Grammar.register0 wit_red_expr (Tactic.red_expr);
+  Grammar.register0 wit_tactic (Tactic.tactic);
+  Grammar.register0 wit_ltac (Tactic.tactic);
+  Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl);
+  Grammar.register0 wit_destruction_arg (Tactic.destruction_arg);
+  ()
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
deleted file mode 100644
index 32dbeaa4..00000000
--- a/parsing/pcoq.ml4
+++ /dev/null
@@ -1,836 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Compat
-open Errors
-open Util
-open Extend
-open Genarg
-open Stdarg
-open Constrarg
-open Tok (* necessary for camlp4 *)
-
-(** The parser of Coq *)
-
-module G = GrammarMake (Lexer)
-
-(* TODO: this is a workaround, since there isn't such
-   [warning_verbose] in new camlp4. In camlp5, this ref
-   gets hidden by [Gramext.warning_verbose] *)
-let warning_verbose = ref true
-
-IFDEF CAMLP5 THEN
-open Gramext
-ELSE
-open PcamlSig.Grammar
-open G
-END
-
-(** Compatibility with Camlp5 6.x *)
-
-IFDEF CAMLP5_6_00 THEN
-let slist0sep x y = Slist0sep (x, y, false)
-let slist1sep x y = Slist1sep (x, y, false)
-ELSE
-let slist0sep x y = Slist0sep (x, y)
-let slist1sep x y = Slist1sep (x, y)
-END
-
-let gram_token_of_token tok =
-IFDEF CAMLP5 THEN
- Stoken (Tok.to_pattern tok)
-ELSE
- match tok with
-  | KEYWORD s -> Skeyword s
-  | tok -> Stoken ((=) tok, to_string tok)
-END
-
-let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
-
-let camlp4_verbosity silent f x =
-  let a = !warning_verbose in
-  warning_verbose := silent;
-  f x;
-  warning_verbose := a
-
-let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
-
-
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-type prod_entry_key =
-  | Alist1 of prod_entry_key
-  | Alist1sep of prod_entry_key * string
-  | Alist0 of prod_entry_key
-  | Alist0sep of prod_entry_key * string
-  | Aopt of prod_entry_key
-  | Amodifiers of prod_entry_key
-  | Aself
-  | Anext
-  | Atactic of int
-  | Agram of string
-  | Aentry of string * string
-
-(** [grammar_object] is the superclass of all grammar entries *)
-
-module type Gramobj =
-sig
-  type grammar_object
-  val weaken_entry : 'a G.entry -> grammar_object G.entry
-end
-
-module Gramobj : Gramobj =
-struct
-  type grammar_object = Obj.t
-  let weaken_entry e = Obj.magic e
-end
-
-(** Grammar entries with associated types *)
-
-type entry_type = argument_type
-type grammar_object = Gramobj.grammar_object
-type typed_entry = argument_type * grammar_object G.entry
-let in_typed_entry t e = (t,Gramobj.weaken_entry e)
-let type_of_typed_entry (t,e) = t
-let object_of_typed_entry (t,e) = e
-let weaken_entry x = Gramobj.weaken_entry x
-
-module type Gramtypes =
-sig
-  val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry
-  val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry
-end
-
-module Gramtypes : Gramtypes =
-struct
-  let inGramObj rawwit = in_typed_entry (unquote rawwit)
-  let outGramObj (a:'a raw_abstract_argument_type) o =
-    if not (argument_type_eq (type_of_typed_entry o) (unquote a))
-      then anomaly ~label:"outGramObj" (str "wrong type");
-    (* downcast from grammar_object *)
-    Obj.magic (object_of_typed_entry o)
-end
-
-open Gramtypes
-
-(** Grammar extensions *)
-
-(** NB: [extend_statment =
-         gram_position option * single_extend_statment list]
-    and [single_extend_statment =
-         string option * gram_assoc option * production_rule list]
-    and [production_rule = symbol list * action]
-
-    In [single_extend_statement], first two parameters are name and
-    assoc iff a level is created *)
-
-(** Type of reinitialization data *)
-type gram_reinit = gram_assoc * gram_position
-
-type ext_kind =
-  | ByGrammar of
-      grammar_object G.entry
-      * gram_reinit option (** for reinitialization if ever needed *)
-      * G.extend_statment
-  | ByEXTEND of (unit -> unit) * (unit -> unit)
-
-(** The list of extensions *)
-
-let camlp4_state = ref []
-
-(** Deletion *)
-
-let grammar_delete e reinit (pos,rls) =
-  List.iter
-    (fun (n,ass,lev) ->
-      List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
-    (List.rev rls);
-  match reinit with
-  | Some (a,ext) ->
-    let lev = match pos with Some (Level n) -> n | _ -> assert false in
-    maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]])
-  | None -> ()
-
-(** The apparent parser of Coq; encapsulate G to keep track
-    of the extensions. *)
-
-module Gram =
-  struct
-    include G
-    let extend e =
-      maybe_curry
-	(fun ext ->
-	   camlp4_state :=
-	     (ByEXTEND ((fun () -> grammar_delete e None ext),
-			(fun () -> maybe_uncurry (G.extend e) ext)))
-	   :: !camlp4_state;
-	   maybe_uncurry (G.extend e) ext)
-    let delete_rule e pil =
-      (* spiwack: if you use load an ML module which contains GDELETE_RULE
-	  in a section, God kills a kitty. As it would corrupt remove_grammars.
-          There does not seem to be a good way to undo a delete rule. As deleting
-	  takes fewer arguments than extending. The production rule isn't returned
-	  by delete_rule. If we could retrieve the necessary information, then
-	  ByEXTEND provides just the framework we need to allow this in section.
-	  I'm not entirely sure it makes sense, but at least it would be more correct.
-          *)
-      G.delete_rule e pil
-  end
-
-(** This extension command is used by the Grammar constr *)
-
-let grammar_extend e reinit ext =
-  camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
-  camlp4_verbose (maybe_uncurry (G.extend e)) ext
-
-(** Remove extensions
-
-   [n] is the number of extended entries (not the number of Grammar commands!)
-   to remove. *)
-
-let rec remove_grammars n =
-  if n>0 then
-    (match !camlp4_state with
-       | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove")
-       | ByGrammar(g,reinit,ext)::t ->
-           let f (a,b) = (of_coq_assoc a, of_coq_position b) in
-           grammar_delete g (Option.map f reinit) ext;
-           camlp4_state := t;
-           remove_grammars (n-1)
-       | ByEXTEND (undo,redo)::t ->
-           undo();
-           camlp4_state := t;
-           remove_grammars n;
-           redo();
-           camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
-
-(** An entry that checks we reached the end of the input. *)
-
-let eoi_entry en =
-  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
-  GEXTEND Gram
-    e: [ [ x = en; EOI -> x ] ]
-    ;
-  END;
-  e
-
-let map_entry f en =
-  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
-  GEXTEND Gram
-    e: [ [ x = en -> f x ] ]
-    ;
-  END;
-  e
-
-(* Parse a string, does NOT check if the entire string was read
-   (use eoi_entry) *)
-
-let parse_string f x =
-  let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
-
-type gram_universe = string * (string, typed_entry) Hashtbl.t
-
-let trace = ref false
-
-(* The univ_tab is not part of the state. It contains all the grammars that
-   exist or have existed before in the session. *)
-
-let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t)
-
-let create_univ s =
-  let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
-
-let uprim   = create_univ "prim"
-let uconstr = create_univ "constr"
-let utactic = create_univ "tactic"
-let uvernac = create_univ "vernac"
-
-let get_univ s =
-  try
-    Hashtbl.find univ_tab s
-  with Not_found ->
-    anomaly (Pp.str ("Unknown grammar universe: "^s))
-
-let get_entry (u, utab) s = Hashtbl.find utab s
-
-let new_entry etyp (u, utab) s =
-  if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr);
-  let ename = u ^ ":" ^ s in
-  let e = in_typed_entry etyp (Gram.entry_create ename) in
-  Hashtbl.add utab s e; e
-
-let create_entry (u, utab) s etyp =
-  try
-    let e = Hashtbl.find utab s in
-    if not (argument_type_eq (type_of_typed_entry e) etyp) then
-      failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
-    e
-  with Not_found ->
-    new_entry etyp (u, utab) s
-
-let create_constr_entry s =
-  outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType)
-
-let create_generic_entry s wit =
-  outGramObj wit (create_entry utactic s (unquote wit))
-
-(* [make_gen_entry] builds entries extensible by giving its name (a string) *)
-(* For entries extensible only via the ML name, Gram.entry_create is enough *)
-
-let make_gen_entry (u,univ) rawwit s =
-  let e = Gram.entry_create (u ^ ":" ^ s) in
-  Hashtbl.add univ s (inGramObj rawwit e); e
-
-(* Initial grammar entries *)
-
-module Prim =
-  struct
-    let gec_gen x = make_gen_entry uprim x
-
-    (* Entries that can be referred via the string -> Gram.entry table *)
-    (* Typically for tactic or vernac extensions *)
-    let preident = gec_gen (rawwit wit_pre_ident) "preident"
-    let ident = gec_gen (rawwit wit_ident) "ident"
-    let natural = gec_gen (rawwit wit_int) "natural"
-    let integer = gec_gen (rawwit wit_int) "integer"
-    let bigint = Gram.entry_create "Prim.bigint"
-    let string = gec_gen (rawwit wit_string) "string"
-    let reference = make_gen_entry uprim (rawwit wit_ref) "reference"
-    let by_notation = Gram.entry_create "by_notation"
-    let smart_global = Gram.entry_create "smart_global"
-
-    (* parsed like ident but interpreted as a term *)
-    let var = gec_gen (rawwit wit_var) "var"
-
-    let name = Gram.entry_create "Prim.name"
-    let identref = Gram.entry_create "Prim.identref"
-    let pattern_ident = Gram.entry_create "pattern_ident"
-    let pattern_identref = Gram.entry_create "pattern_identref"
-
-    (* A synonym of ident - maybe ident will be located one day *)
-    let base_ident = Gram.entry_create "Prim.base_ident"
-
-    let qualid = Gram.entry_create "Prim.qualid"
-    let fullyqualid = Gram.entry_create "Prim.fullyqualid"
-    let dirpath = Gram.entry_create "Prim.dirpath"
-
-    let ne_string = Gram.entry_create "Prim.ne_string"
-    let ne_lstring = Gram.entry_create "Prim.ne_lstring"
-
-  end
-
-module Constr =
-  struct
-    let gec_constr = make_gen_entry uconstr (rawwit wit_constr)
-
-    (* Entries that can be referred via the string -> Gram.entry table *)
-    let constr = gec_constr "constr"
-    let operconstr = gec_constr "operconstr"
-    let constr_eoi = eoi_entry constr
-    let lconstr = gec_constr "lconstr"
-    let binder_constr = create_constr_entry "binder_constr"
-    let ident = make_gen_entry uconstr (rawwit wit_ident) "ident"
-    let global = make_gen_entry uconstr (rawwit wit_ref) "global"
-    let sort = make_gen_entry uconstr (rawwit wit_sort) "sort"
-    let pattern = Gram.entry_create "constr:pattern"
-    let constr_pattern = gec_constr "constr_pattern"
-    let lconstr_pattern = gec_constr "lconstr_pattern"
-    let closed_binder = Gram.entry_create "constr:closed_binder"
-    let binder = Gram.entry_create "constr:binder"
-    let binders = Gram.entry_create "constr:binders"
-    let open_binders = Gram.entry_create "constr:open_binders"
-    let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
-    let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
-    let record_declaration = Gram.entry_create "constr:record_declaration"
-    let appl_arg = Gram.entry_create "constr:appl_arg"
-  end
-
-module Module =
-  struct
-    let module_expr = Gram.entry_create "module_expr"
-    let module_type = Gram.entry_create "module_type"
-  end
-
-module Tactic =
-  struct
-    (* Main entry for extensions *)
-    let simple_tactic = Gram.entry_create "tactic:simple_tactic"
-
-    (* Entries that can be referred via the string -> Gram.entry table *)
-    (* Typically for tactic user extensions *)
-    let open_constr =
-      make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
-    let constr_with_bindings =
-      make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
-    let bindings =
-      make_gen_entry utactic (rawwit wit_bindings) "bindings"
-    let hypident = Gram.entry_create "hypident"
-    let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
-    let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
-    let uconstr =
-      make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
-    let quantified_hypothesis =
-      make_gen_entry utactic (rawwit wit_quant_hyp) "quantified_hypothesis"
-    let int_or_var = make_gen_entry utactic (rawwit wit_int_or_var) "int_or_var"
-    let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr"
-    let simple_intropattern =
-      make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern"
-    let clause_dft_concl = 
-      make_gen_entry utactic (rawwit wit_clause_dft_concl) "clause"
-
-
-    (* Main entries for ltac *)
-    let tactic_arg = Gram.entry_create "tactic:tactic_arg"
-    let tactic_expr = Gram.entry_create "tactic:tactic_expr"
-    let binder_tactic = Gram.entry_create "tactic:binder_tactic"
-
-    let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
-
-    (* Main entry for quotations *)
-    let tactic_eoi = eoi_entry tactic
-
-    (* For Ltac definition *)
-    let tacdef_body = Gram.entry_create "tactic:tacdef_body"
-
-  end
-
-module Vernac_ =
-  struct
-    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
-
-    (* The different kinds of vernacular commands *)
-    let gallina = gec_vernac "gallina"
-    let gallina_ext = gec_vernac "gallina_ext"
-    let command = gec_vernac "command"
-    let syntax = gec_vernac "syntax_command"
-    let vernac = gec_vernac "Vernac.vernac"
-    let vernac_eoi = eoi_entry vernac
-    let rec_definition = gec_vernac "Vernac.rec_definition"
-    (* Main vernac entry *)
-    let main_entry = Gram.entry_create "vernac"
-
-    GEXTEND Gram
-    main_entry:
-      [ [ a = vernac -> Some (!@loc, a) | EOI -> None ] ]
-    ;
-    END
-
-  end
-
-let main_entry = Vernac_.main_entry
-
-(**********************************************************************)
-(* This determines (depending on the associativity of the current
-   level and on the expected associativity) if a reference to constr_n is
-   a reference to the current level (to be translated into "SELF" on the
-   left border and into "constr LEVEL n" elsewhere), to the level below
-   (to be translated into "NEXT") or to an below wrt associativity (to be
-   translated in camlp4 into "constr" without level) or to another level
-   (to be translated into "constr LEVEL n")
-
-   The boolean is true if the entry was existing _and_ empty; this to
-   circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the
-   converse of the extension mechanism *)
-
-let constr_level = string_of_int
-
-let default_levels =
-  [200,Extend.RightA,false;
-   100,Extend.RightA,false;
-   99,Extend.RightA,true;
-   10,Extend.RightA,false;
-   9,Extend.RightA,false;
-   8,Extend.RightA,true;
-   1,Extend.LeftA,false;
-   0,Extend.RightA,false]
-
-let default_pattern_levels =
-  [200,Extend.RightA,true;
-   100,Extend.RightA,false;
-   99,Extend.RightA,true;
-   11,Extend.LeftA,false;
-   10,Extend.RightA,false;
-   1,Extend.LeftA,false;
-   0,Extend.RightA,false]
-
-let level_stack =
-  ref [(default_levels, default_pattern_levels)]
-
-(* At a same level, LeftA takes precedence over RightA and NoneA *)
-(* In case, several associativity exists for a level, we make two levels, *)
-(* first LeftA, then RightA and NoneA together *)
-
-let admissible_assoc = function
-  | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false
-  | Extend.RightA, Some Extend.LeftA -> false
-  | _ -> true
-
-let create_assoc = function
-  | None -> Extend.RightA
-  | Some a -> a
-
-let error_level_assoc p current expected =
-  let pr_assoc = function
-    | Extend.LeftA -> str "left"
-    | Extend.RightA -> str "right"
-    | Extend.NonA -> str "non" in
-  errorlabstrm ""
-    (str "Level " ++ int p ++ str " is already declared " ++
-     pr_assoc current ++ str " associative while it is now expected to be " ++
-     pr_assoc expected ++ str " associative.")
-
-let create_pos = function
-  | None -> Extend.First
-  | Some lev -> Extend.After (constr_level lev)
-
-let find_position_gen forpat ensure assoc lev =
-  let ccurrent,pcurrent as current = List.hd !level_stack in
-  match lev with
-  | None ->
-      level_stack := current :: !level_stack;
-      None, None, None, None
-  | Some n ->
-      let after = ref None in
-      let init = ref None in
-      let rec add_level q = function
-        | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
-        | (p,a,reinit)::l when Int.equal p n ->
-            if reinit then
-	      let a' = create_assoc assoc in
-              (init := Some (a',create_pos q); (p,a',false)::l)
-	    else if admissible_assoc (a,assoc) then
-	      raise Exit
-            else
-	      error_level_assoc p a (Option.get assoc)
-	| l -> after := q; (n,create_assoc assoc,ensure)::l
-      in
-      try
-	let updated =
-	  if forpat then (ccurrent, add_level None pcurrent)
-	  else (add_level None ccurrent, pcurrent) in
-        level_stack := updated:: !level_stack;
-	let assoc = create_assoc assoc in
-        begin match !init with
-        | None ->
-	  (* Create the entry *)
-	   Some (create_pos !after), Some assoc, Some (constr_level n), None
-        | _ ->
-	  (* The reinit flag has been updated *)
-	   Some (Extend.Level (constr_level n)), None, None, !init
-        end
-      with
-	  (* Nothing has changed *)
-          Exit ->
-            level_stack := current :: !level_stack;
-	    (* Just inherit the existing associativity and name (None) *)
-	    Some (Extend.Level (constr_level n)), None, None, None
-
-let remove_levels n =
-  level_stack := List.skipn n !level_stack
-
-let rec list_mem_assoc_triple x = function
-  | [] -> false
-  | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l
-
-let register_empty_levels forpat levels =
-  let filter n =
-    try
-      let levels = (if forpat then snd else fst) (List.hd !level_stack) in
-      if not (list_mem_assoc_triple n levels) then
-        Some (find_position_gen forpat true None (Some n))
-      else None
-    with Failure _ -> None
-  in
-  List.map_filter filter levels
-
-let find_position forpat assoc level =
-  find_position_gen forpat false assoc level
-
-(* Synchronise the stack of level updates *)
-let synchronize_level_positions () =
-  let _ = find_position true None None in ()
-
-(**********************************************************************)
-(* Binding constr entry keys to entries                               *)
-
-(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
-let camlp4_assoc = function
-  | Some Extend.NonA | Some Extend.RightA -> Extend.RightA
-  | None | Some Extend.LeftA -> Extend.LeftA
-
-let assoc_eq al ar = match al, ar with
-| Extend.NonA, Extend.NonA
-| Extend.RightA, Extend.RightA
-| Extend.LeftA, Extend.LeftA -> true
-| _, _ -> false
-
-(* [adjust_level assoc from prod] where [assoc] and [from] are the name
-   and associativity of the level where to add the rule; the meaning of
-   the result is
-
-     None = SELF
-     Some None = NEXT
-     Some (Some (n,cur)) = constr LEVEL n
-         s.t. if [cur] is set then [n] is the same as the [from] level *)
-let adjust_level assoc from = function
-(* Associativity is None means force the level *)
-  | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
-(* Compute production name on the right side *)
-  (* If NonA or LeftA on the right-hand side, set to NEXT *)
-  | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) ->
-      Some None
-  (* If RightA on the right-hand side, set to the explicit (current) level *)
-  | (NumLevel n,BorderProd (Right,Some Extend.RightA)) ->
-      Some (Some (n,true))
-(* Compute production name on the left side *)
-  (* If NonA on the left-hand side, adopt the current assoc ?? *)
-  | (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None
-  (* If the expected assoc is the current one, set to SELF *)
-  | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) ->
-      None
-  (* Otherwise, force the level, n or n-1, according to expected assoc *)
-  | (NumLevel n,BorderProd (Left,Some a)) ->
-    begin match a with
-    | Extend.LeftA -> Some (Some (n, true))
-    | _ -> Some None
-    end
-  (* None means NEXT *)
-  | (NextLevel,_) -> Some None
-(* Compute production name elsewhere *)
-  | (NumLevel n,InternalProd) ->
-      match from with
-	| ETConstr (p,()) when Int.equal p (n + 1) -> Some None
-	| ETConstr (p,()) -> Some (Some (n, Int.equal n p))
-	| _ -> Some (Some (n,false))
-
-let compute_entry allow_create adjust forpat = function
-  | ETConstr (n,q) ->
-      (if forpat then weaken_entry Constr.pattern
-       else weaken_entry Constr.operconstr),
-      adjust (n,q), false
-  | ETName -> weaken_entry Prim.name, None, false
-  | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList")
-  | ETBinder false -> weaken_entry Constr.binder, None, false
-  | ETBinderList (true,tkl) ->
-    let () = match tkl with [] -> () | _ -> assert false in
-    weaken_entry Constr.open_binders, None, false
-  | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.")
-  | ETBigint -> weaken_entry Prim.bigint, None, false
-  | ETReference -> weaken_entry Constr.global, None, false
-  | ETPattern -> weaken_entry Constr.pattern, None, false
-  | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
-  | ETOther (u,n) ->
-      let u = get_univ u in
-      let e =
-        try get_entry u n
-        with Not_found when allow_create -> create_entry u n ConstrArgType in
-      object_of_typed_entry e, None, true
-
-(* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key forpat = function
-  | ETConstr(200,()) when not forpat ->
-      weaken_entry Constr.binder_constr, None
-  | e ->
-      let (e,level,_) = compute_entry true (fun (n,()) -> Some n) forpat e in
-      (e, level)
-
-(* This computes the name to give to a production knowing the name and
-   associativity of the level where it must be added *)
-let interp_constr_prod_entry_key ass from forpat en =
-  compute_entry false (adjust_level ass from) forpat en
-
-(**********************************************************************)
-(* Binding constr entry keys to symbols                               *)
-
-let is_self from e =
-  match from, e with
-      ETConstr(n,()), ETConstr(NumLevel n',
-        BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false
-    | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n'
-    | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint
-      | ETPattern, ETPattern) -> true
-    | ETOther(s1,s2), ETOther(s1',s2') ->
-      String.equal s1 s1' && String.equal s2 s2'
-    | _ -> false
-
-let is_binder_level from e =
-  match from, e with
-      ETConstr(200,()),
-      ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true
-    | _ -> false
-
-let make_sep_rules tkl =
-  Gram.srules'
-    [List.map gram_token_of_token tkl,
-     List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
-       (Gram.action (fun loc -> ()))]
-
-let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
-  if is_binder_level from typ then
-    if forpat then
-      Snterml (Gram.Entry.obj Constr.pattern,"200")
-    else
-      Snterml (Gram.Entry.obj Constr.operconstr,"200")
-  else if is_self from typ then
-      Sself
-  else
-    match typ with
-    | ETConstrList (typ',[]) ->
-        Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
-    | ETConstrList (typ',tkl) ->
-        slist1sep
-          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
-          (make_sep_rules tkl)
-    | ETBinderList (false,[]) ->
-        Slist1
-	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
-    | ETBinderList (false,tkl) ->
-        slist1sep
-          (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
-          (make_sep_rules tkl)
-
-    | _ ->
-    match interp_constr_prod_entry_key assoc from forpat typ with
-      | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj)
-      | (eobj,Some None,_) -> Snext
-      | (eobj,Some (Some (lev,cur)),_) ->
-          Snterml (Gram.Entry.obj eobj,constr_level lev)
-
-(** Binding general entry keys to symbol *)
-
-let rec symbol_of_prod_entry_key = function
-  | Alist1 s -> Slist1 (symbol_of_prod_entry_key s)
-  | Alist1sep (s,sep) ->
-      slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
-  | Alist0 s -> Slist0 (symbol_of_prod_entry_key s)
-  | Alist0sep (s,sep) ->
-      slist0sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
-  | Aopt s -> Sopt (symbol_of_prod_entry_key s)
-  | Amodifiers s ->
-       Gram.srules'
-        [([], Gram.action (fun _loc -> []));
-         ([gram_token_of_string "(";
-           slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string ",");
-           gram_token_of_string ")"],
-	   Gram.action (fun _ l _ _loc -> l))]
-  | Aself -> Sself
-  | Anext -> Snext
-  | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic)
-  | Atactic n ->
-      Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
-  | Agram s ->
-    let e =
-      try
-      (** ppedrot: we should always generate Agram entries which have already
-          been registered, so this should not fail. *)
-        let (u, s) = match String.split ':' s with
-        | u :: s :: [] -> (u, s)
-        | _ -> raise Not_found
-        in
-        get_entry (get_univ u) s
-      with Not_found ->
-        Errors.anomaly (str "Unregistered grammar entry: " ++ str s)
-    in
-    Snterm (Gram.Entry.obj (object_of_typed_entry e))
-  | Aentry (u,s) ->
-    let e = get_entry (get_univ u) s in
-    Snterm (Gram.Entry.obj (object_of_typed_entry e))
-
-let level_of_snterml = function
-  | Snterml (_,l) -> int_of_string l
-  | _ -> failwith "level_of_snterml"
-
-(**********************************************************************)
-(* Interpret entry names of the form "ne_constr_list" as entry keys   *)
-
-let coincide s pat off =
-  let len = String.length pat in
-  let break = ref true in
-  let i = ref 0 in
-  while !break && !i < len do
-    let c = Char.code s.[off + !i] in
-    let d = Char.code pat.[!i] in
-    break := Int.equal c d;
-    incr i
-  done;
-  !break
-
-let tactic_level s =
-  if Int.equal (String.length s) 7 && coincide s "tactic" 0 then
-    let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
-    else None
-  else None
-
-let type_of_entry u s =
-  type_of_typed_entry (get_entry u s)
-
-let rec interp_entry_name static up_level s sep =
-  let l = String.length s in
-  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
-    ListArgType t, Alist1 g
-  else if l > 12 && coincide s "ne_" 0 &&
-                   coincide s "_list_sep" (l-9) then
-    let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
-    ListArgType t, Alist1sep (g,sep)
-  else if l > 5 && coincide s "_list" (l-5) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
-    ListArgType t, Alist0 g
-  else if l > 9 && coincide s "_list_sep" (l-9) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
-    ListArgType t, Alist0sep (g,sep)
-  else if l > 4 && coincide s "_opt" (l-4) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
-    OptArgType t, Aopt g
-  else if l > 5 && coincide s "_mods" (l-5) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
-    ListArgType t, Amodifiers g
-  else
-    let s = match s with "hyp" -> "var" | _ -> s in
-    let check_lvl n = match up_level with
-    | None -> false
-    | Some m -> Int.equal m n
-                && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
-                && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
-    in
-    let t, se =
-      match tactic_level s with
-      | Some n ->
-        (** Quite ad-hoc *)
-        let t = unquote (rawwit wit_tactic) in
-        let se =
-          if check_lvl n then Aself
-          else if check_lvl (n + 1) then Anext
-          else Atactic n
-        in
-        (Some t, se)
-      | None ->
-      try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found ->
-      try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found ->
-      try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found ->
-	if static then
-	  error ("Unknown entry "^s^".")
-	else
-	  None, Aentry ("",s) in
-    let t =
-      match t with
-	| Some t -> t
-	| None -> ExtraArgType s in
-    t, se
-
-let list_entry_names () =
-  let add_entry key (entry, _) accu = (key, entry) :: accu in
-  let ans = Hashtbl.fold add_entry (snd uprim) [] in
-  let ans = Hashtbl.fold add_entry (snd uconstr) ans in
-  Hashtbl.fold add_entry (snd utactic) ans
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 24b58775..37165f6c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -14,13 +14,12 @@ open Genarg
 open Constrexpr
 open Tacexpr
 open Libnames
-open Compat
 open Misctypes
 open Genredexpr
 
 (** The parser of Coq *)
 
-module Gram : GrammarSig
+module Gram : module type of Compat.GrammarMake(CLexer)
 
 (** The parser of Coq is built from three kinds of rule declarations:
 
@@ -40,7 +39,7 @@ module Gram : GrammarSig
         |     (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
         |
@@ -97,38 +96,7 @@ module Gram : GrammarSig
 
 *)
 
-val gram_token_of_token : Tok.t -> Gram.symbol
-val gram_token_of_string : string -> Gram.symbol
-
-(** The superclass of all grammar entries *)
-type grammar_object
-
-(** Type of reinitialization data *)
-type gram_reinit = gram_assoc * gram_position
-
-(** Add one extension at some camlp4 position of some camlp4 entry *)
-val grammar_extend :
-  grammar_object Gram.entry ->
-  gram_reinit option (** for reinitialization if ever needed *) ->
-  Gram.extend_statment -> unit
-
-(** Remove the last n extensions *)
-val remove_grammars : int -> unit
-
-
-
-
-(** The type of typed grammar objects *)
-type typed_entry
-
-(** The possible types for extensible grammars *)
-type entry_type = argument_type
-
-val type_of_typed_entry : typed_entry -> entry_type
-val object_of_typed_entry : typed_entry -> grammar_object Gram.entry
-val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry
-
-(** Temporary activate camlp4 verbosity *)
+(** Temporarily activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
@@ -138,12 +106,8 @@ val parse_string : 'a Gram.entry -> string -> 'a
 val eoi_entry : 'a Gram.entry -> 'a Gram.entry
 val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
 
-(** Table of Coq statically defined grammar entries *)
-
 type gram_universe
 
-(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
-
 val get_univ : string -> gram_universe
 
 val uprim : gram_universe
@@ -151,9 +115,11 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
-val create_entry : gram_universe -> string -> entry_type -> typed_entry
-val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
-  'a Gram.entry
+val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
+
+val create_generic_entry : gram_universe -> string ->
+  ('a, rlevel) abstract_argument_type -> 'a Gram.entry
 
 module Prim :
   sig
@@ -163,6 +129,7 @@ module Prim :
     val ident : Id.t Gram.entry
     val name : Name.t located Gram.entry
     val identref : Id.t located Gram.entry
+    val pidentref : (Id.t located * (Id.t located list) option) Gram.entry
     val pattern_ident : Id.t Gram.entry
     val pattern_identref : Id.t located Gram.entry
     val base_ident : Id.t Gram.entry
@@ -190,6 +157,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
@@ -212,7 +180,7 @@ module Module :
 
 module Tactic :
   sig
-    val open_constr : open_constr_expr Gram.entry
+    val open_constr : constr_expr Gram.entry
     val constr_with_bindings : constr_expr with_bindings Gram.entry
     val bindings : constr_expr bindings Gram.entry
     val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
@@ -220,17 +188,18 @@ module Tactic :
     val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
     val uconstr : constr_expr Gram.entry
     val quantified_hypothesis : quantified_hypothesis Gram.entry
+    val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
     val int_or_var : int or_var Gram.entry
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_tactic_expr Gram.entry
     val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
+    val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
     val tactic_expr : raw_tactic_expr Gram.entry
     val binder_tactic : raw_tactic_expr Gram.entry
     val tactic : raw_tactic_expr Gram.entry
     val tactic_eoi : raw_tactic_expr Gram.entry
-    val tacdef_body : (reference * bool * raw_tactic_expr) Gram.entry
   end
 
 module Vernac_ :
@@ -242,69 +211,57 @@ module Vernac_ :
     val vernac : vernac_expr Gram.entry
     val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
     val vernac_eoi : vernac_expr Gram.entry
+    val noedit_mode : vernac_expr Gram.entry
+    val command_entry : vernac_expr Gram.entry
+    val hint_info : Vernacexpr.hint_info_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
 val main_entry : (Loc.t * vernac_expr) option Gram.entry
 
-(** Mapping formal entries into concrete ones *)
-
-(** Binding constr entry keys to entries and symbols *)
-
-val interp_constr_entry_key : bool (** true for cases_pattern *) ->
-  constr_entry_key -> grammar_object Gram.entry * int option
+(** Handling of the proof mode entry *)
+val get_command_entry : unit -> vernac_expr Gram.entry
+val set_command_entry : vernac_expr Gram.entry -> unit
 
-val symbol_of_constr_prod_entry_key : gram_assoc option ->
-  constr_entry_key -> bool -> constr_prod_entry_key ->
-    Gram.symbol
+val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
-(** General entry keys *)
+(** {5 Extending the parser without synchronization} *)
 
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-type prod_entry_key =
-  | Alist1 of prod_entry_key
-  | Alist1sep of prod_entry_key * string
-  | Alist0 of prod_entry_key
-  | Alist0sep of prod_entry_key * string
-  | Aopt of prod_entry_key
-  | Amodifiers of prod_entry_key
-  | Aself
-  | Anext
-  | Atactic of int
-  | Agram of string
-  | Aentry of string * string
-
-(** Binding general entry keys to symbols *)
+type gram_reinit = gram_assoc * gram_position
+(** Type of reinitialization data *)
 
-val symbol_of_prod_entry_key :
-  prod_entry_key -> Gram.symbol
+val grammar_extend : 'a Gram.entry -> gram_reinit option ->
+  'a Extend.extend_statment -> unit
+(** Extend the grammar of Coq, without synchronizing it with the backtracking
+    mechanism. This means that grammar extensions defined this way will survive
+    an undo. *)
 
-(** Interpret entry names of the form "ne_constr_list" as entry keys   *)
+(** {5 Extending the parser with summary-synchronized commands} *)
 
-val interp_entry_name : bool (** true to fail on unknown entry *) ->
-  int option -> string -> string -> entry_type * prod_entry_key
+module GramState : Store.S
+(** Auxiliary state of the grammar. Any added data must be marshallable. *)
 
-(** Recover the list of all known tactic notation entries. *)
-val list_entry_names : unit -> (string * entry_type) list
+type 'a grammar_command
+(** Type of synchronized parsing extensions. The ['a] type should be
+    marshallable. *)
 
-(** Registering/resetting the level of a constr entry *)
+type extend_rule =
+| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule
 
-val find_position :
-  bool (** true if for creation in pattern entry; false if in constr entry *) ->
-  Extend.gram_assoc option -> int option ->
-    Extend.gram_position option * Extend.gram_assoc option * string option *
-    (** for reinitialization: *) gram_reinit option
+type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
+(** Grammar extension entry point. Given some ['a] and a current grammar state,
+    such a function must produce the list of grammar extensions that will be
+    applied in the same order and kept synchronized w.r.t. the summary, together
+    with a new state. It should be pure. *)
 
-val synchronize_level_positions : unit -> unit
+val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command
+(** Create a new grammar-modifying command with the given name. The extension
+    function is called to generate the rules for a given data. *)
 
-val register_empty_levels : bool -> int list ->
-    (Extend.gram_position option * Extend.gram_assoc option *
-     string option * gram_reinit option) list
+val extend_grammar_command : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
 
-val remove_levels : int -> unit
+val recover_grammar_command : 'a grammar_command -> 'a list
+(** Recover the current stack of grammar extensions. *)
 
-val level_of_snterml : Gram.symbol -> int
+val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/tok.ml b/parsing/tok.ml
index c96b53de..f4b60aee 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -8,9 +8,10 @@
 
 (** The type of token for the Coq lexer and parser *)
 
+let string_equal (s1 : string) s2 = s1 = s2
+
 type t =
   | KEYWORD of string
-  | METAIDENT of string
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
@@ -21,16 +22,15 @@ type t =
   | EOI
 
 let equal t1 t2 = match t1, t2 with
-| IDENT s1, KEYWORD s2 -> CString.equal s1 s2
-| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
-| METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2
-| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
-| IDENT s1, IDENT s2 -> CString.equal s1 s2
-| FIELD s1, FIELD s2 -> CString.equal s1 s2
-| INT s1, INT s2 -> CString.equal s1 s2
-| STRING s1, STRING s2 -> CString.equal s1 s2
+| IDENT s1, KEYWORD s2 -> string_equal s1 s2
+| KEYWORD s1, KEYWORD s2 -> string_equal s1 s2
+| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
+| IDENT s1, IDENT s2 -> string_equal s1 s2
+| FIELD s1, FIELD s2 -> string_equal s1 s2
+| INT s1, INT s2 -> string_equal s1 s2
+| STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
-| BULLET s1, BULLET s2 -> CString.equal s1 s2
+| BULLET s1, BULLET s2 -> string_equal s1 s2
 | EOI, EOI -> true
 | _ -> false
 
@@ -38,7 +38,6 @@ let extract_string = function
   | KEYWORD s -> s
   | IDENT s -> s
   | STRING s -> s
-  | METAIDENT s -> s
   | PATTERNIDENT s -> s
   | FIELD s -> s
   | INT s -> s
@@ -49,13 +48,12 @@ let extract_string = function
 let to_string = function
   | KEYWORD s -> Format.sprintf "%S" s
   | IDENT s -> Format.sprintf "IDENT %S" s
-  | METAIDENT s -> Format.sprintf "METAIDENT %S" s
   | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s
   | FIELD s -> Format.sprintf "FIELD %S" s
   | INT s -> Format.sprintf "INT %s" s
   | STRING s -> Format.sprintf "STRING %S" s
   | LEFTQMARK -> "LEFTQMARK"
-  | BULLET s -> Format.sprintf "STRING %S" s
+  | BULLET s -> Format.sprintf "BULLET %S" s
   | EOI -> "EOI"
 
 let match_keyword kwd = function
@@ -72,7 +70,6 @@ let print ppf tok = Format.pp_print_string ppf (to_string tok)
 let of_pattern = function
   | "", s -> KEYWORD s
   | "IDENT", s -> IDENT s
-  | "METAIDENT", s -> METAIDENT s
   | "PATTERNIDENT", s -> PATTERNIDENT s
   | "FIELD", s -> FIELD s
   | "INT", s -> INT s
@@ -85,7 +82,6 @@ let of_pattern = function
 let to_pattern = function
   | KEYWORD s -> "", s
   | IDENT s -> "IDENT", s
-  | METAIDENT s -> "METAIDENT", s
   | PATTERNIDENT s -> "PATTERNIDENT", s
   | FIELD s -> "FIELD", s
   | INT s -> "INT", s
@@ -99,7 +95,6 @@ let match_pattern =
   function
     | "", "" -> (function KEYWORD s -> s | _ -> err ())
     | "IDENT", "" -> (function IDENT s -> s | _ -> err ())
-    | "METAIDENT", "" -> (function METAIDENT s -> s | _ -> err ())
     | "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ())
     | "FIELD", "" -> (function FIELD s -> s | _ -> err ())
     | "INT", "" -> (function INT s -> s | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index df006601..b9286c53 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -10,7 +10,6 @@
 
 type t =
   | KEYWORD of string
-  | METAIDENT of string
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
@@ -20,6 +19,7 @@ type t =
   | BULLET of string
   | EOI
 
+val equal : t -> t -> bool
 val extract_string : t -> string
 val to_string : t -> string
 (* Needed to fit Camlp4 signature *)