Merge PR #7558: [api] Make `vernac/` self-contained.

10 files changed, 10 insertions, 2507 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
deleted file mode 100644
index 5f63d21c4d..0000000000
--- a/parsing/egramcoq.ml
+++ /dev/null
@@ -1,483 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open CErrors
-open Util
-open Pcoq
-open Constrexpr
-open Notation_term
-open Extend
-open Libnames
-open Names
-
-(**********************************************************************)
-(* 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 camlp5 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 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;
-   90,Extend.RightA,true;
-   10,Extend.LeftA,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;
-   90,Extend.RightA,true;
-   10,Extend.LeftA,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
-  user_err 
-    (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 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)
-
-(**************************************************************************)
-(*
- * --- Note on the mapping of grammar productions to camlp5 actions ---
- *
- * Translation of environments: a production
- *   [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
- * is written (with camlp5 conventions):
- *   (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
- * where v1..vi are the values generated by non-terminals nt1..nti.
- * Since the actions are executed by substituting an environment,
- * the make_*_action family build the following closure:
- *
- *      ((fun env ->
- *          (fun vi ->
- *             (fun env -> ...
- *
- *                  (fun v1 ->
- *                     (fun env -> gram_action .. env act)
- *                     ((x1,v1)::env))
- *                  ...)
- *             ((xi,vi)::env)))
- *         [])
- *)
-
-(**********************************************************************)
-(** Declare Notations grammar rules                                   *)
-
-(**********************************************************************)
-(* Binding constr entry keys to entries                               *)
-
-(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *)
-let camlp5_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 (camlp5_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, Misctypes.lname) entry
-| TTReference : ('self, reference) entry
-| TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTConstr : prod_info * 'r target -> ('r, 'r) entry
-| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
-| TTPattern : int -> ('self, cases_pattern_expr) entry
-| TTOpenBinderList : ('self, local_binder_expr list) entry
-| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr 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 = function
-  | [tk] -> Atoken tk
-  | tkl ->
-  let rec mkrule : Tok.t list -> string rules = function
-  | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "")
-  | 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)
-| TTPattern p -> Aentryl (Constr.pattern, p)
-| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
-| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
-| TTName -> Aentry Prim.name
-| TTOpenBinderList -> Aentry Constr.open_binders
-| TTBigint -> Aentry Prim.bigint
-| TTReference -> Aentry Constr.global
-
-let interp_entry forpat e = match e with
-| ETProdName -> TTAny TTName
-| ETProdReference -> TTAny TTReference
-| ETProdBigint -> TTAny TTBigint
-| ETProdConstr p -> TTAny (TTConstr (p, forpat))
-| ETProdPattern p -> TTAny (TTPattern p)
-| ETProdOther _ -> assert false (** not used *)
-| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
-| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
-| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
-
-let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
-  | Anonymous -> CPatAtom None
-  | Name id   -> CPatAtom (Some (CAst.make ?loc @@ Ident id))
-
-type 'r env = {
-  constrs : 'r list;
-  constrlists : 'r list list;
-  binders : cases_pattern_expr list;
-  binderlists : local_binder_expr list list;
-}
-
-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 -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders }
-  | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
-  end
-| TTPattern _ ->
-  begin match forpat with
-  | ForConstr -> { subst with binders = v :: subst.binders }
-  | ForPattern -> push_constr subst v
-  end
-| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
-| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
-| TTBigint ->
-  begin match forpat with
-  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true)))
-  end
-| TTReference ->
-  begin match forpat with
-  | ForConstr  -> push_constr subst (CAst.make @@ CRef (v, None))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatAtom (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 * int * ('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, p, rem) ->
-  fun f env ->
-    let heads, constrs = List.chop n env.constrs in
-    let constrlists, constrs =
-      if b then
-         (* We rearrange constrs = c1..cn rem and constrlists = [d1..dr e1..ep] rem' into
-            constrs = e1..ep rem and constrlists [c1..cn d1..dr] rem' *)
-         let constrlist = List.hd env.constrlists in
-         let constrlist, tail = List.chop (List.length constrlist - p) constrlist in
-         (heads @ constrlist) :: List.tl env.constrlists, tail @ constrs
-      else
-         (* We rearrange constrs = c1..cn e1..ep rem into
-            constrs = e1..ep rem and add a constr list [c1..cn] *)
-        let constrlist, tail = List.chop (n - p) heads in
-        constrlist :: env.constrlists, tail @ constrs
-    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, p) :: rem ->
-    let AnyTyRule r = make_ty_rule rem in
-    AnyTyRule (TyMark (n, b, p, r))
-  in
-  make_ty_rule (List.rev prods)
-
-let target_to_bool : type r. r target -> bool = function
-| ForConstr -> false
-| ForPattern -> true
-
-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, env.binders, env.binderlists) in
-  CAst.make ~loc @@ CNotation (notation, env)
-| ForPattern -> fun notation loc env ->
-  let env = (env.constrs, env.constrlists) in
-  CAst.make ~loc @@ CPatNotation (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 = []; binderlists = [] } 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 constr_levels = GramState.field ()
-
-let extend_constr_notation ng state =
-  let levels = match GramState.get state constr_levels with
-  | None -> default_constr_levels
-  | Some lev -> lev
-  in
-  (* 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 constr_grammar : one_notation_grammar grammar_command =
-  create_grammar_command "Notation" extend_constr_notation
-
-let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
deleted file mode 100644
index e15add10f6..0000000000
--- a/parsing/egramcoq.mli
+++ /dev/null
@@ -1,19 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Mapping of grammar productions to camlp5 actions *)
-
-(** This is the part specific to Coq-level Notation and Tactic Notation.
-    For the ML-level tactic and vernac extensions, see Egramml. *)
-
-(** {5 Adding notations} *)
-
-val extend_constr_grammar : Notation_term.one_notation_grammar -> unit
-(** Add a term notation rule to the parsing system. *)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
deleted file mode 100644
index 90cd7d10b7..0000000000
--- a/parsing/egramml.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Extend
-open Pcoq
-open Genarg
-open Vernacexpr
-
-(** Grammar extensions declared at ML level *)
-
-type 's grammar_prod_item =
-  | GramTerminal of string
-  | GramNonTerminal :
-      ('a raw_abstract_argument_type option * ('s, 'a) symbol) Loc.located -> '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 = Option.map (fun t obj -> Genarg.in_gen t obj) t 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 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 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 *)
-
-let vernac_exts = ref []
-
-let get_extend_vernac_rule (s, i) =
-  try
-    let find ((name, j), _) = String.equal name s && Int.equal i j in
-    let (_, rules) = List.find find !vernac_exts in
-    rules
-  with
-  | Failure _ -> raise Not_found
-
-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, l) in
-  let rules = [make_rule mkact gl] in
-  grammar_extend nt None (None, [None, None, rules])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
deleted file mode 100644
index 31aa1a9891..0000000000
--- a/parsing/egramml.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Vernacexpr
-
-(** Mapping of grammar productions to camlp5 actions. *)
-
-(** This is the part specific to vernac extensions.
-    For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
-
-type 's grammar_prod_item =
-  | GramTerminal of string
-  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option *
-      ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
-
-val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
-    vernac_expr grammar_prod_item list -> unit
-
-val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
-
-(** Utility function reused in Egramcoq : *)
-
-val make_rule :
-  (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
-  'a grammar_prod_item list -> 'a Extend.production_rule
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
deleted file mode 100644
index 4f3d83a8a6..0000000000
--- a/parsing/g_proofs.ml4
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Constrexpr
-open Vernacexpr
-open Proof_global
-open Misctypes
-
-open Pcoq
-open Pcoq.Prim
-open Pcoq.Constr
-open Pcoq.Vernac_
-
-let thm_token = G_vernac.thm_token
-
-let hint = Gram.entry_create "hint"
-
-let warn_deprecated_focus =
-  CWarnings.create ~name:"deprecated-focus" ~category:"deprecated"
-         (fun () ->
-           Pp.strbrk
-             "The Focus command is deprecated; use bullets or focusing brackets instead"
-         )
-
-let warn_deprecated_focus_n n =
-  CWarnings.create ~name:"deprecated-focus" ~category:"deprecated"
-         (fun () ->
-           Pp.(str "The Focus command is deprecated;" ++ spc ()
-               ++ str "use '" ++ int n ++ str ": {' instead")
-         )
-
-let warn_deprecated_unfocus =
-  CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated"
-         (fun () -> Pp.strbrk "The Unfocus command is deprecated")
-
-(* Proof commands *)
-GEXTEND Gram
-  GLOBAL: hint command;
-
-  opt_hintbases:
-  [ [ -> []
-    | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
-  ;
-  command:
-    [ [ IDENT "Goal"; c = lconstr ->
-        VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c))
-      | IDENT "Proof" -> VernacProof (None,None)
-      | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
-      | IDENT "Proof"; c = lconstr -> VernacExactProof c
-      | IDENT "Abort" -> VernacAbort None
-      | IDENT "Abort"; IDENT "All" -> VernacAbortAll
-      | IDENT "Abort"; id = identref -> VernacAbort (Some id)
-      | IDENT "Existential"; n = natural; c = constr_body ->
-	  VernacSolveExistential (n,c)
-      | IDENT "Admitted" -> VernacEndProof Admitted
-      | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None))
-      | IDENT "Save"; id = identref ->
-	  VernacEndProof (Proved (Opaque, Some id))
-      | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
-      |	IDENT "Defined"; id=identref ->
-	  VernacEndProof (Proved (Transparent,Some id))
-      | IDENT "Restart" -> VernacRestart
-      | IDENT "Undo" -> VernacUndo 1
-      | IDENT "Undo"; n = natural -> VernacUndo n
-      | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n
-      | IDENT "Focus" ->
-         warn_deprecated_focus ~loc:!@loc ();
-         VernacFocus None
-      | IDENT "Focus"; n = natural ->
-         warn_deprecated_focus_n n ~loc:!@loc ();
-         VernacFocus (Some n)
-      | IDENT "Unfocus" ->
-         warn_deprecated_unfocus ~loc:!@loc ();
-         VernacUnfocus
-      | IDENT "Unfocused" -> VernacUnfocused
-      | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
-      | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
-      | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
-      | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
-      | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
-      | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses
-      | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
-      | 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 = reference -> VernacShow (ShowMatch id)
-      | IDENT "Guarded" -> VernacCheckGuard
-      (* Hints for Auto and EAuto *)
-      | IDENT "Create"; IDENT "HintDb" ;
-	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
-	    VernacCreateHintDb (id, b)
-      | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
-	  VernacRemoveHints (dbnames, ids)
-      | IDENT "Hint"; h = hint;
-	  dbnames = opt_hintbases ->
-          VernacHints (dbnames, h)
-      (* Declare "Resolve" explicitly so as to be able to later extend with
-         "Resolve ->" and "Resolve <-" *)
-      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; 
-	info = hint_info; dbnames = opt_hintbases ->
-          VernacHints (dbnames,
-	    HintsResolve (List.map (fun x -> (info, true, x)) lc))
-      ] ];
-  reference_or_constr:
-   [ [ r = global -> HintsReference r
-     | c = constr -> HintsConstr c ] ]
-  ;
-  hint:
-    [ [ 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)
-      | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m)
-      | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
-      | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ]
-    ;
-  constr_body:
-    [ [ ":="; c = lconstr -> c
-      | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ]
-  ;
-  mode:
-    [ [ l = LIST1 [ "+" -> ModeInput
-                  | "!" -> ModeNoHeadEvar
-                  | "-" -> ModeOutput ] -> l ] ]
-  ;
-END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
deleted file mode 100644
index a1c563f536..0000000000
--- a/parsing/g_vernac.ml4
+++ /dev/null
@@ -1,1154 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Util
-open Names
-open Vernacexpr
-open Constrexpr
-open Constrexpr_ops
-open Extend
-open Decl_kinds
-open Declaremods
-open Declarations
-open Misctypes
-open Tok (* necessary for camlp5 *)
-
-open Pcoq
-open Pcoq.Prim
-open Pcoq.Constr
-open Pcoq.Vernac_
-open Pcoq.Module
-
-let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
-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 subprf = Gram.entry_create "vernac:subprf"
-
-let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
-let thm_token = Gram.entry_create "vernac:thm_token"
-let def_body = Gram.entry_create "vernac:def_body"
-let decl_notation = Gram.entry_create "vernac:decl_notation"
-let record_field = Gram.entry_create "vernac:record_field"
-let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
-let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
-
-let make_bullet s =
-  let open Proof_bullet in
-  let n = String.length s in
-  match s.[0] with
-  | '-' -> Dash n
-  | '+' -> Plus n
-  | '*' -> Star n
-  | _ -> assert false
-
-let parse_compat_version ?(allow_old = true) = let open Flags in function
-  | "8.8" -> Current
-  | "8.7" -> V8_7
-  | "8.6" -> V8_6
-  | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
-    CErrors.user_err ~hdr:"get_compat_version"
-      Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s ->
-    CErrors.user_err ~hdr:"get_compat_version"
-      Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
-
-GEXTEND Gram
-  GLOBAL: vernac_control gallina_ext noedit_mode subprf;
-  vernac_control: FIRST
-    [ [ IDENT "Time"; c = located_vernac -> VernacTime (false,c)
-      | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
-      | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v)
-      | IDENT "Fail"; v = vernac_control -> VernacFail v
-      | (f, v) = vernac -> VernacExpr(f, v) ]
-    ]
-  ;
-  vernac:
-    [ [ IDENT "Local"; (f, v) = vernac_poly -> (VernacLocal true :: f, v)
-      | IDENT "Global"; (f, v) = vernac_poly -> (VernacLocal false :: f, v)
-
-      | v = vernac_poly -> v ]
-    ]
-  ;
-  vernac_poly:
-    [ [ IDENT "Polymorphic"; (f, v) = vernac_aux -> (VernacPolymorphic true :: f, v)
-      | IDENT "Monomorphic"; (f, v) = vernac_aux -> (VernacPolymorphic false :: f, v)
-      | v = vernac_aux -> v ]
-    ]
-  ;
-  vernac_aux:
-    (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
-    (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> ([VernacProgram], g)
-      | IDENT "Program"; g = gallina_ext; "." -> ([VernacProgram], g)
-      | g = gallina; "." -> ([], g)
-      | g = gallina_ext; "." -> ([], g)
-      | c = command; "." -> ([], c)
-      | c = syntax; "." -> ([], c)
-      | c = subprf -> ([], c)
-    ] ]
-  ;
-  vernac_aux: LAST
-    [ [ prfcom = command_entry -> ([], prfcom) ] ]
-  ;
-  noedit_mode:
-    [ [ c = query_command -> c None] ]
-  ;
-
-  subprf:
-  [ [ s = BULLET -> VernacBullet (make_bullet s)
-    | "{" -> VernacSubproof None
-    | "}" -> VernacEndSubproof
-    ] ]
-  ;
-
-  located_vernac:
-    [ [ v = vernac_control -> CAst.make ~loc:!@loc v ] ]
-  ;
-END
-
-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
-  | [(_,([_],_))] ->
-     warn_plural_command ~loc:!@loc kwd
-  | _ -> ()
-
-let test_plural_form_types loc kwd = function
-  | [([_],_)] ->
-     warn_plural_command ~loc:!@loc kwd
-  | _ -> ()
-
-let lname_of_lident : lident -> lname =
-  CAst.map (fun s -> Name s)
-
-let name_of_ident_decl : ident_decl -> name_decl =
-  on_fst lname_of_lident
-
-(* Gallina declarations *)
-GEXTEND Gram
-  GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    record_field decl_notation rec_definition ident_decl univ_decl;
-
-  gallina:
-      (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr;
-        l = LIST0
-          [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr ->
-          (id,(bl,c)) ] ->
-          VernacStartTheoremProof (thm, (id,(bl,c))::l)
-      | stre = assumption_token; nl = inline; bl = assum_list ->
-	  VernacAssumption (stre, nl, bl)
-      | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
-	  test_plural_form loc kwd bl;
-	  VernacAssumption (stre, nl, bl)
-      | d = def_token; id = ident_decl; b = def_body ->
-          VernacDefinition (d, name_of_ident_decl id, b)
-      | IDENT "Let"; id = identref; b = def_body ->
-          VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b)
-      (* Gallina inductive declarations *)
-      | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
-        indl = LIST1 inductive_definition SEP "with" ->
-	  let (k,f) = f in
-          let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-          VernacInductive (cum, priv,f,indl)
-      | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (NoDischarge, recs)
-      | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (DoDischarge, recs)
-      | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (NoDischarge, corecs)
-      | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (DoDischarge, corecs)
-      | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
-      | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
-	      l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
-      | IDENT "Register"; IDENT "Inline"; id = identref ->
-          VernacRegister(id, RegisterInline)
-      | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l
-      | IDENT "Universes"; l = LIST1 identref -> VernacUniverse l
-      | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l
-  ] ]
-  ;
-
-  thm_token:
-    [ [ "Theorem" -> Theorem
-      | IDENT "Lemma" -> Lemma
-      | IDENT "Fact" -> Fact
-      | IDENT "Remark" -> Remark
-      | IDENT "Corollary" -> Corollary
-      | IDENT "Proposition" -> Proposition
-      | IDENT "Property" -> Property ] ]
-  ;
-  def_token:
-    [ [ "Definition" -> (NoDischarge,Definition)
-      | IDENT "Example" -> (NoDischarge,Example)
-      | IDENT "SubClass" -> (NoDischarge,SubClass) ] ]
-  ;
-  assumption_token:
-    [ [ "Hypothesis" -> (DoDischarge, Logical)
-      | "Variable" -> (DoDischarge, Definitional)
-      | "Axiom" -> (NoDischarge, Logical)
-      | "Parameter" -> (NoDischarge, Definitional)
-      | IDENT "Conjecture" -> (NoDischarge, Conjectural) ] ]
-  ;
-  assumptions_token:
-    [ [ IDENT "Hypotheses" -> ("Hypotheses", (DoDischarge, Logical))
-      | IDENT "Variables" -> ("Variables", (DoDischarge, Definitional))
-      | IDENT "Axioms" -> ("Axioms", (NoDischarge, Logical))
-      | IDENT "Parameters" -> ("Parameters", (NoDischarge, Definitional))
-      | IDENT "Conjectures" -> ("Conjectures", (NoDischarge, Conjectural)) ] ]
-  ;
-  inline:
-    [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
-      | IDENT "Inline" -> DefaultInline
-      | -> NoInline] ]
-  ;
-  univ_constraint:
-    [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
-	r = universe_level -> (l, ord, r) ] ]
-  ;
-  univ_decl :
-    [ [  "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ];
-         cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
-                ext = [ "+" -> true | -> false ]; "}" -> (l',ext)
-              | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ]
-         ->
-         { univdecl_instance = l;
-           univdecl_extensible_instance = ext;
-           univdecl_constraints = fst cs;
-           univdecl_extensible_constraints = snd cs }
-    ] ]
-  ;
-  ident_decl:
-    [ [ i = identref; l = OPT univ_decl -> (i, l)
-  ] ]
-  ;
-  finite_token:
-    [ [ IDENT "Inductive" -> (Inductive_kw,Finite)
-      | IDENT "CoInductive" -> (CoInductive,CoFinite)
-      | IDENT "Variant" -> (Variant,BiFinite)
-      | IDENT "Record" -> (Record,BiFinite)
-      | IDENT "Structure" -> (Structure,BiFinite)
-      | IDENT "Class" -> (Class true,BiFinite) ] ]
-  ;
-  cumulativity_token:
-    [ [ IDENT "Cumulative" -> VernacCumulative
-      | IDENT "NonCumulative" -> VernacNonCumulative ] ]
-  ;
-  private_token:
-    [ [ IDENT "Private" -> true | -> false ] ]
-  ;
-  (* Simple definitions *)
-  def_body:
-    [ [ bl = binders; ":="; red = reduce; c = lconstr ->
-      if List.exists (function CLocalPattern _ -> true | _ -> false) bl
-      then
-        (* FIXME: "red" will be applied to types in bl and Cast with remain *)
-        let c = mkCLambdaN ~loc:!@loc bl c in
-	DefineBody ([], red, c, None)
-      else
-        (match c with
-        | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t)
-        | _ -> DefineBody (bl, red, c, None))
-    | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
-        let ((bl, c), tyo) =
-          if List.exists (function CLocalPattern _ -> true | _ -> false) bl
-          then
-            (* FIXME: "red" will be applied to types in bl and Cast with remain *)
-            let c = CAst.make ~loc:!@loc @@ CCast (c, CastConv t) in
-            (([],mkCLambdaN ~loc:!@loc bl c), None)
-          else ((bl, c), Some t)
-        in
-	DefineBody (bl, red, c, tyo)
-    | bl = binders; ":"; t = lconstr ->
-        ProveBody (bl, t) ] ]
-  ;
-  reduce:
-    [ [ IDENT "Eval"; r = red_expr; "in" -> Some r
-      | -> None ] ]
-  ;
-  one_decl_notation:
-    [ [ ntn = ne_lstring; ":="; c = constr;
-        scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ]
-  ;
-  decl_notation:
-    [ [ "where"; l = LIST1 one_decl_notation SEP IDENT "and" -> l
-    | -> [] ] ]
-  ;
-  (* Inductives and records *)
-  opt_constructors_or_fields:
-    [ [ ":="; lc = constructor_list_or_record_decl -> lc
-      | -> RecordDecl (None, []) ] ]
-  ;
-  inductive_definition:
-    [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
-        c = OPT [ ":"; c = lconstr -> c ];
-        lc=opt_constructors_or_fields; ntn = decl_notation ->
-	   (((oc,id),indpar,c,lc),ntn) ] ]
-  ;
-  constructor_list_or_record_decl:
-    [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
-      | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
-	  Constructors ((c id)::l)
-      | id = identref ; c = constructor_type -> Constructors [ c id ]
-      | cstr = identref; "{"; fs = record_fields; "}" ->
-	  RecordDecl (Some cstr,fs)
-      | "{";fs = record_fields; "}" -> RecordDecl (None,fs)
-      |  -> Constructors [] ] ]
-  ;
-(*
-  csort:
-    [ [ s = sort -> CSort (loc,s) ] ]
-  ;
-*)
-  opt_coercion:
-    [ [ ">" -> true
-      |  -> false ] ]
-  ;
-  (* (co)-fixpoints *)
-  rec_definition:
-    [ [ id = ident_decl;
-	bl = binders_fixannot;
-        ty = type_cstr;
-	def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
-	  let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
-  ;
-  corec_definition:
-    [ [ id = ident_decl; bl = binders; ty = type_cstr;
-        def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
-          ((id,bl,ty,def),ntn) ] ]
-  ;
-  type_cstr:
-    [ [ ":"; c=lconstr -> c
-      | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ]
-  ;
-  (* Inductive schemes *)
-  scheme:
-    [ [ kind = scheme_kind -> (None,kind)
-      | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ]
-  ;
-  scheme_kind:
-    [ [ IDENT "Induction"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s)
-      | IDENT "Minimality"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s)
-      | IDENT "Elimination"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s)
-      | IDENT "Case"; "for"; ind = smart_global;
-          IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s)
-      | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ]
-  ;
-  (* Various Binders *)
-(*
-  (* ... without coercions *)
-  binder_nodef:
-    [ [ b = binder_let ->
-      (match b with
-          CLocalAssum(l,ty) -> (l,ty)
-        | CLocalDef _ ->
-            Util.user_err_loc
-              (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ]
-  ;
-*)
-  (* ... with coercions *)
-  record_field:
-  [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ];
-      ntn = decl_notation -> (bd,pri),ntn ] ]
-  ;
-  record_fields:
-    [ [ f = record_field; ";"; fs = record_fields -> f :: fs
-      | f = record_field; ";" -> [f]
-      | f = record_field -> [f]
-      | -> []
-    ] ]
-  ;
-  record_binder_body:
-    [ [ l = binders; oc = of_type_with_opt_coercion;
-         t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN ~loc:!@loc l t))
-      | l = binders; oc = of_type_with_opt_coercion;
-         t = lconstr; ":="; b = lconstr -> fun id ->
-	   (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t)))
-      | l = binders; ":="; b = lconstr -> fun id ->
-         match b.CAst.v with
-	 | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
-	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t)))
-         | _ ->
-	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ]
-  ;
-  record_binder:
-    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))
-      | id = name; f = record_binder_body -> f id ] ]
-  ;
-  assum_list:
-    [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ]
-  ;
-  assum_coe:
-    [ [ "("; a = simple_assum_coe; ")" -> a ] ]
-  ;
-  simple_assum_coe:
-    [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
-        (not (Option.is_empty oc),(idl,c)) ] ]
-  ;
-
-  constructor_type:
-    [[ l = binders;
-      t= [ coe = of_type_with_opt_coercion; c = lconstr ->
-	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c))
-            |  ->
-		 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
-	 -> t l
-     ]]
-;
-
-  constructor:
-    [ [ id = identref; c=constructor_type -> c id ] ]
-  ;
-  of_type_with_opt_coercion:
-    [ [ ":>>" -> Some false
-	| ":>"; ">" -> Some false
-	| ":>" -> Some true
-	| ":"; ">"; ">" -> Some false
-	| ":"; ">" -> Some true
-	| ":" -> None ] ]
-  ;
-END
-
-let only_starredidentrefs =
-  Gram.Entry.of_parser "test_only_starredidentrefs"
-    (fun strm ->
-      let rec aux n =
-      match Util.stream_nth n strm with
-        | KEYWORD "." -> ()
-        | KEYWORD ")" -> ()
-        | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
-        | _ -> raise Stream.Failure in
-      aux 0)
-let starredidentreflist_to_expr l =
-  match l with
-  | [] -> 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;
-
-  gallina_ext:
-    [ [ (* Interactive module declaration *)
-        IDENT "Module"; export = export_token; id = identref;
-	bl = LIST0 module_binder; sign = of_module_type;
-	body = is_module_expr ->
-	  VernacDefineModule (export, id, bl, sign, body)
-      | IDENT "Module"; "Type"; id = identref;
-	bl = LIST0 module_binder; sign = check_module_types;
-	body = is_module_type ->
-	  VernacDeclareModuleType (id, bl, sign, body)
-      | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
-	bl = LIST0 module_binder; ":"; mty = module_type_inl ->
-	  VernacDeclareModule (export, id, bl, mty)
-      (* Section beginning *)
-      | IDENT "Section"; id = identref -> VernacBeginSection id
-      | IDENT "Chapter"; id = identref -> VernacBeginSection id
-
-      (* This end a Section a Module or a Module Type *)
-      | IDENT "End"; id = identref -> VernacEndSegment id
-
-      (* Naming a set of section hyps *)
-      | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
-          VernacNameSectionHypSet (id, expr)
-
-      (* Requiring an already compiled module *)
-      | IDENT "Require"; export = export_token; qidl = LIST1 global ->
-          VernacRequire (None, export, qidl)
-      | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token
-	; qidl = LIST1 global ->
-	VernacRequire (Some ns, export, qidl)
-      | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
-      | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
-      | 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 ->
-	 warn_deprecated_include_type ~loc:!@loc ();
-	 VernacInclude(e::l) ] ]
-  ;
-  export_token:
-    [ [ IDENT "Import" -> Some false
-      | IDENT "Export" -> Some true
-      |  -> None ] ]
-  ;
-  ext_module_type:
-    [ [ "<+"; mty = module_type_inl -> mty ] ]
-  ;
-  ext_module_expr:
-    [ [ "<+"; mexpr = module_expr_inl -> mexpr ] ]
-  ;
-  check_module_type:
-    [ [ "<:"; mty = module_type_inl -> mty ] ]
-  ;
-  check_module_types:
-    [ [ mtys = LIST0 check_module_type -> mtys ] ]
-  ;
-  of_module_type:
-    [ [ ":"; mty = module_type_inl -> Enforce mty
-      | mtys = check_module_types -> Check mtys ] ]
-  ;
-  is_module_type:
-    [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> (mty::l)
-      | -> [] ] ]
-  ;
-  is_module_expr:
-    [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l)
-      | -> [] ] ]
-  ;
-  functor_app_annot:
-    [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" ->
-        InlineAt (int_of_string i)
-      | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline
-      | -> DefaultInline
-      ] ]
-  ;
-  module_expr_inl:
-    [ [ "!"; me = module_expr -> (me,NoInline)
-      | me = module_expr; a = functor_app_annot -> (me,a) ] ]
-  ;
-  module_type_inl:
-    [ [ "!"; me = module_type -> (me,NoInline)
-      | me = module_type; a = functor_app_annot -> (me,a) ] ]
-  ;
-  (* Module binder  *)
-  module_binder:
-    [ [ "("; export = export_token; idl = LIST1 identref; ":";
-         mty = module_type_inl; ")" -> (export,idl,mty) ] ]
-  ;
-  (* Module expressions *)
-  module_expr:
-    [ [ me = module_expr_atom -> me
-      | me1 = module_expr; me2 = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (me1,me2)
-      ] ]
-  ;
-  module_expr_atom:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
-  ;
-  with_declaration:
-    [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
-          CWith_Definition (fqid,udecl,c)
-      | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
-	  CWith_Module (fqid,qid)
-      ] ]
-  ;
-  module_type:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
-      | "("; mt = module_type; ")" -> mt
-      | mty = module_type; me = module_expr_atom ->
-          CAst.make ~loc:!@loc @@ CMapply (mty,me)
-      | mty = module_type; "with"; decl = with_declaration ->
-          CAst.make ~loc:!@loc @@ CMwith (mty,decl)
-      ] ]
-  ;
-  (* Proof using *)
-  section_subset_expr:
-    [ [ only_starredidentrefs; l = LIST0 starredidentref ->
-          starredidentreflist_to_expr l
-      | e = ssexpr -> e ]]
-  ;
-  starredidentref:
-    [ [ i = identref -> SsSingl i
-      | i = identref; "*" -> SsFwdClose(SsSingl i)
-      | "Type" -> SsType
-      | "Type"; "*" -> SsFwdClose SsType ]]
-  ;
-  ssexpr:
-    [ "35" 
-      [ "-"; e = ssexpr -> SsCompl e ]
-    | "50"
-      [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
-      | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
-    | "0"
-      [ i = starredidentref -> i
-      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
-          starredidentreflist_to_expr l
-      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
-          SsFwdClose(starredidentreflist_to_expr l)
-      | "("; e = ssexpr; ")"-> e 
-      | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
-  ;
-END
-
-(* Extensions: implicits, coercions, etc. *)
-GEXTEND Gram
-  GLOBAL: gallina_ext instance_name hint_info;
-
-  gallina_ext:
-    [ [ (* Transparent and Opaque *)
-        IDENT "Transparent"; l = LIST1 smart_global ->
-          VernacSetOpacity (Conv_oracle.transparent, l)
-      | IDENT "Opaque"; l = LIST1 smart_global ->
-          VernacSetOpacity (Conv_oracle.Opaque, l)
-      | IDENT "Strategy"; l =
-          LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] ->
-            VernacSetStrategy l
-      (* Canonical structure *)
-      | IDENT "Canonical"; IDENT "Structure"; qid = global ->
-          VernacCanonical CAst.(make ~loc:!@loc @@ AN qid)
-      | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
-          VernacCanonical CAst.(make ~loc:!@loc @@ ByNotation ntn)
-      | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
-          let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d)
-
-      (* Coercions *)
-      | IDENT "Coercion"; qid = global; d = def_body ->
-          let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d)
-      | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
-         s = class_rawexpr; ">->"; t = class_rawexpr ->
-           VernacIdentityCoercion (f, s, t)
-      | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
-         t = class_rawexpr ->
-          VernacCoercion (CAst.make ~loc:!@loc @@ AN qid, s, t)
-      | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->";
-         t = class_rawexpr ->
-          VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t)
-
-      | IDENT "Context"; c = binders ->
-	  VernacContext c
-
-      | IDENT "Instance"; namesup = instance_name; ":";
-	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
-	 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,info)
-
-      | IDENT "Existing"; IDENT "Instance"; id = global;
-          info = hint_info ->
-	  VernacDeclareInstances [id, info]
-
-      | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
-        pri = OPT [ "|"; i = natural -> i ] ->
-         let info = { Typeclasses.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; 
-        args = LIST0 argument_spec_block;
-        more_implicits = OPT
-          [ ","; impl = LIST1
-            [ impl = LIST0 more_implicits_block -> List.flatten impl]
-            SEP "," -> impl
-          ];
-        mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
-         let mods = match mods with None -> [] | Some l -> List.flatten l in
-         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
-                user_err Pp.(str "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)
-
-      | IDENT "Implicit"; "Type"; bl = reserv_list ->
-	   VernacReserve bl
-
-      | IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
-          test_plural_form_types loc "Implicit Types" bl;
-           VernacReserve bl
-
-      | IDENT "Generalizable"; 
-	   gen = [IDENT "All"; IDENT "Variables" -> Some []
-	     | IDENT "No"; IDENT "Variables" -> None
-	     | ["Variable" | IDENT "Variables"];
-		  idl = LIST1 identref -> Some idl ] ->
-	     VernacGeneralizable gen ] ]
-  ;
-  arguments_modifier:
-    [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase]
-      | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold]
-      | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
-      | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
-      | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
-      | IDENT "rename" -> [`Rename]
-      | IDENT "assert" -> [`Assert]
-      | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes]
-      | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
-          [`ClearImplicits; `ClearScopes]
-      | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
-          [`ClearImplicits; `ClearScopes]
-      ] ]
-  ;
-  scope:
-    [ [ "%"; key = IDENT -> key ] ]
-  ;
-  argument_spec: [
-       [ b = OPT "!"; id = name ; s = OPT scope ->
-       id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc:!@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 -> CAst.make ~loc:!@loc y) x
-         | Some _, Some _ -> user_err Pp.(str "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 -> CAst.make ~loc:!@loc y) x
-         | Some _, Some _ -> user_err Pp.(str "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 -> CAst.make ~loc:!@loc y) x
-         | Some _, Some _ -> user_err Pp.(str "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
-    ]
-  ];
-  (* Same as [argument_spec_block], but with only implicit status and names *)
-  more_implicits_block: [
-    [ name = name -> [(name.CAst.v, Vernacexpr.NotImplicit)]
-    | "["; items = LIST1 name; "]" ->
-       List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items
-    | "{"; items = LIST1 name; "}" ->
-       List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items
-    ]
-  ];
-  strategy_level:
-    [ [ IDENT "expand" -> Conv_oracle.Expand
-      | IDENT "opaque" -> Conv_oracle.Opaque
-      | n=INT -> Conv_oracle.Level (int_of_string n)
-      | "-"; n=INT -> Conv_oracle.Level (- int_of_string n)
-      | IDENT "transparent" -> Conv_oracle.transparent ] ]
-  ;
-  instance_name:
-    [ [ name = ident_decl; sup = OPT binders ->
-          (CAst.map (fun id -> Name id) (fst name), snd name),
-          (Option.default [] sup)
-      | -> ((CAst.make ~loc:!@loc Anonymous), None), []  ] ]
-  ;
-  hint_info:
-    [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
-         { Typeclasses.hint_priority = i; hint_pattern = pat }
-      | -> { Typeclasses.hint_priority = None; hint_pattern = None } ] ]
-  ;
-  reserv_list:
-    [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
-  ;
-  reserv_tuple:
-    [ [ "("; a = simple_reserv; ")" -> a ] ]
-  ;
-  simple_reserv:
-    [ [ idl = LIST1 identref; ":"; c = lconstr -> (idl,c) ] ]
-  ;
-
-END
-
-GEXTEND Gram
-  GLOBAL: command query_command class_rawexpr gallina_ext;
-
-  gallina_ext:
-    [ [ IDENT "Export"; "Set"; table = option_table; v = option_value ->
-        VernacSetOption (true, table, v)
-      | IDENT "Export"; IDENT "Unset"; table = option_table ->
-          VernacUnsetOption (true, table)
-    ] ];
-
-  command:
-    [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
-
-      (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
-      | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
-	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
-	 info = hint_info ->
-	   VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info)
-
-      (* System directory *)
-      | IDENT "Pwd" -> VernacChdir None
-      | IDENT "Cd" -> VernacChdir None
-      | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir)
-
-      | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ];
-	s = [ s = ne_string -> s | s = IDENT -> s ] ->
-	  VernacLoad (verbosely, s)
-      | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
-	  VernacDeclareMLModule l
-
-      | IDENT "Locate"; l = locatable -> VernacLocate l
-
-      (* Managing load paths *)
-      | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
-	  VernacAddLoadPath (false, dir, alias)
-      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
-	  alias = as_dirpath -> VernacAddLoadPath (true, dir, alias)
-      | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
-	  VernacRemoveLoadPath dir
-
-       (* For compatibility *)
-      | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath ->
-	  VernacAddLoadPath (false, dir, alias)
-      | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath ->
-	  VernacAddLoadPath (true, dir, alias)
-      | IDENT "DelPath"; dir = ne_string ->
-	  VernacRemoveLoadPath dir
-
-      (* Type-Checking (pas dans le refman) *)
-      | "Type"; c = lconstr -> VernacGlobalCheck c
-
-      (* Printing (careful factorization of entries) *)
-      | IDENT "Print"; p = printable -> VernacPrint p
-      | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> VernacPrint (PrintName (qid,l))
-      | IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
-	  VernacPrint (PrintModuleType qid)
-      | IDENT "Print"; IDENT "Module"; qid = global ->
-	  VernacPrint (PrintModule qid)
-      | IDENT "Print"; IDENT "Namespace" ; ns = dirpath ->
-          VernacPrint (PrintNamespace ns)
-      | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
-
-      | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
-	  VernacAddMLPath (false, dir)
-      | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
-	  VernacAddMLPath (true, dir)
-
-      (* For acting on parameter tables *)
-      | "Set"; table = option_table; v = option_value ->
-          VernacSetOption (false, table, v)
-      | IDENT "Unset"; table = option_table ->
-          VernacUnsetOption (false, table)
-
-      | IDENT "Print"; IDENT "Table"; table = option_table ->
-	  VernacPrintOption table
-
-      | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
-        -> VernacAddOption ([table;field], v)
-      (* A global value below will be hidden by a field above! *)
-      (* In fact, we give priority to secondary tables *)
-      (* No syntax for tertiary tables due to conflict *)
-      (* (but they are unused anyway) *)
-      | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
-          VernacAddOption ([table], v)
-
-      | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value
-        -> VernacMemOption (table, v)
-      | IDENT "Test"; table = option_table ->
-          VernacPrintOption table
-
-      | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
-        -> VernacRemoveOption ([table;field], v)
-      | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
-	  VernacRemoveOption ([table], v) ]] 
-  ;
-  query_command: (* TODO: rapprocher Eval et Check *)
-    [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." ->
-          fun g -> VernacCheckMayEval (Some r, g, c)
-      | IDENT "Compute"; c = lconstr; "." ->
-	  fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c)
-      | IDENT "Check"; c = lconstr; "." ->
-	 fun g -> VernacCheckMayEval (None, g, c)
-      (* Searching the environment *)
-      | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
-         fun g -> VernacPrint (PrintAbout (qid,l,g))
-      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
-	  fun g -> VernacSearch (SearchHead c,g, l)
-      | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
-	  fun g -> VernacSearch (SearchPattern c,g, l)
-      | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
-	  fun g -> VernacSearch (SearchRewrite c,g, l)
-      | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." ->
-	  let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m)
-      (* compatibility: SearchAbout *)
-      | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." ->
-	  fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m)
-      (* compatibility: SearchAbout with "[ ... ]" *)
-      | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
-	l = in_or_out_modules; "." ->
-         fun g -> VernacSearch (SearchAbout sl,g, l)
-      ] ]
-  ;
-  printable:
-    [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> PrintName (qid,l)
-      | IDENT "All" -> PrintFullContext
-      | IDENT "Section"; s = global -> PrintSectionContext s
-      | IDENT "Grammar"; ent = IDENT ->
-          (* This should be in "syntax" section but is here for factorization*)
-	  PrintGrammar ent
-      | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir
-      | IDENT "Modules" ->
-          user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead")
-      | IDENT "Libraries" -> PrintModules
-
-      | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath
-      | IDENT "ML"; IDENT "Modules" -> PrintMLModules
-      | IDENT "Debug"; IDENT "GC" -> PrintDebugGC
-      | IDENT "Graph" -> PrintGraph
-      | IDENT "Classes" ->  PrintClasses
-      | IDENT "TypeClasses" -> PrintTypeClasses
-      | IDENT "Instances"; qid = smart_global -> PrintInstances qid
-      | IDENT "Coercions" -> PrintCoercions
-      | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
-         -> PrintCoercionPaths (s,t)
-      | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions
-      | IDENT "Tables" -> PrintTables
-      | IDENT "Options" -> PrintTables (* A Synonymous to Tables *)
-      | IDENT "Hint" -> PrintHintGoal
-      | IDENT "Hint"; qid = smart_global -> PrintHint qid
-      | IDENT "Hint"; "*" -> PrintHintDb
-      | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
-      | IDENT "Scopes" -> PrintScopes
-      | IDENT "Scope"; s = IDENT -> PrintScope s
-      | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s
-      | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid
-      | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt)
-      | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt)
-      | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, false, qid)
-      | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, false, qid)
-      | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (false, true, qid)
-      | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid)
-      | IDENT "Strategy"; qid = smart_global -> PrintStrategy (Some qid)
-      | IDENT "Strategies" -> PrintStrategy None ] ]
-  ;
-  class_rawexpr:
-    [ [ IDENT "Funclass" -> FunClass
-      | IDENT "Sortclass" -> SortClass
-      | qid = smart_global -> RefClass qid ] ]
-  ;
-  locatable:
-    [ [ qid = smart_global -> LocateAny qid
-      | IDENT "Term"; qid = smart_global -> LocateTerm qid
-      | IDENT "File"; f = ne_string -> LocateFile f
-      | IDENT "Library"; qid = global -> LocateLibrary qid
-      | IDENT "Module"; qid = global -> LocateModule qid ] ]
-  ;
-  option_value:
-    [ [ -> BoolValue true
-      | n  = integer   -> IntValue (Some n)
-      | s  = STRING    -> StringValue s ] ]
-  ;
-  option_ref_value:
-    [ [ id = global   -> QualidRefValue id
-      | s  = STRING   -> StringRefValue s ] ]
-  ;
-  option_table:
-    [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]]
-  ;
-  as_dirpath:
-    [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
-  ;
-  ne_in_or_out_modules:
-    [ [ IDENT "inside"; l = LIST1 global -> SearchInside l
-      | IDENT "outside"; l = LIST1 global -> SearchOutside l ] ]
-  ;
-  in_or_out_modules:
-    [ [ m = ne_in_or_out_modules -> m
-      | -> SearchOutside [] ] ]
-  ;
-  comment:
-    [ [ c = constr -> CommentConstr c
-      | s = STRING -> CommentString s
-      | n = natural -> CommentInt n ] ]
-  ;
-  positive_search_mark:
-    [ [ "-" -> false | -> true ] ]
-  ;
-  scope:
-    [ [ "%"; key = IDENT -> key ] ]
-  ;
-  searchabout_query:
-    [ [ b = positive_search_mark; s = ne_string; sc = OPT scope ->
-            (b, SearchString (s,sc))
-      | b = positive_search_mark; p = constr_pattern ->
-            (b, SearchSubPattern p)
-      ] ]
-  ;
-  searchabout_queries:
-    [ [ m = ne_in_or_out_modules -> ([],m)
-      | s = searchabout_query; l = searchabout_queries ->
-        let (sl,m) = l in (s::sl,m)
-      | -> ([],SearchOutside [])
-      ] ]
-  ;
-  univ_name_list:
-    [ [  "@{" ; l = LIST0 name; "}" -> l ] ]
-  ;
-END;
-
-GEXTEND Gram
-  command:
-    [ [
-(* State management *)
-        IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s
-      | IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s
-      | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s
-      | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s
-
-(* Resetting *)
-      | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
-      | IDENT "Reset"; id = identref -> VernacResetName id
-      | IDENT "Back" -> VernacBack 1
-      | IDENT "Back"; n = natural -> VernacBack n
-      | IDENT "BackTo"; n = natural -> VernacBackTo n
-
-(* Tactic Debugger *)
-      |	IDENT "Debug"; IDENT "On" ->
-          VernacSetOption (false, ["Ltac";"Debug"], BoolValue true)
-
-      |	IDENT "Debug"; IDENT "Off" ->
-          VernacSetOption (false, ["Ltac";"Debug"], BoolValue false)
-
-(* registration of a custom reduction *)
-
-      | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":=";
-         r = red_expr ->
-	   VernacDeclareReduction (s,r)
-
- ] ];
-    END
-;;
-
-(* Grammar extensions *)
-
-GEXTEND Gram
-  GLOBAL: syntax;
-
-  syntax:
-   [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (true,sc)
-
-     | IDENT "Close"; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (false,sc)
-
-     | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
-	 VernacDelimiters (sc, Some key)
-     | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT ->
-	 VernacDelimiters (sc, None)
-
-     | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
-       refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
-
-     | IDENT "Infix"; op = ne_lstring; ":="; p = constr;
-         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
-	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix ((op,modl),p,sc)
-     | IDENT "Notation"; id = identref;
-	 idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
-           VernacSyntacticDefinition
-             (id,(idl,c),b)
-     | IDENT "Notation"; s = lstring; ":=";
-	 c = constr;
-         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
-	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (c,(s,modl),sc)
-     | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
-           VernacNotationAddFormat (n,s,fmt)
-
-     | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
-	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
-           let s = CAst.map (fun s -> "x '"^s^"' y") s in
-           VernacSyntaxExtension (true,(s,l))
-
-     | IDENT "Reserved"; IDENT "Notation";
-	 s = ne_lstring;
-	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-         -> VernacSyntaxExtension (false, (s,l))
-
-     (* "Print" "Grammar" should be here but is in "command" entry in order
-        to factorize with other "Print"-based vernac entries *)
-  ] ]
-  ;
-  only_parsing:
-    [ [ "("; IDENT "only"; IDENT "parsing"; ")" ->
-         Some Flags.Current
-      | "("; IDENT "compat"; s = STRING; ")" ->
-         Some (parse_compat_version s)
-      | -> None ] ]
-  ;
-  level:
-    [ [ IDENT "level"; n = natural -> NumLevel n
-      | IDENT "next"; IDENT "level" -> NextLevel ] ]
-  ;
-  syntax_modifier:
-    [ [ "at"; IDENT "level"; n = natural -> SetLevel n
-      | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA
-      | IDENT "right"; IDENT "associativity" -> SetAssoc RightA
-      | IDENT "no"; IDENT "associativity" -> SetAssoc NonA
-      | IDENT "only"; IDENT "printing" -> SetOnlyPrinting
-      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
-      | IDENT "compat"; s = STRING ->
-        SetCompatVersion (parse_compat_version s)
-      | IDENT "format"; s1 = [s = STRING -> CAst.make ~loc:!@loc s];
-                        s2 = OPT [s = STRING -> CAst.make ~loc:!@loc s] ->
-          begin match s1, s2 with
-          | { CAst.v = k }, Some s -> SetFormat(k,s)
-          | s, None -> SetFormat ("text",s) end
-      | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
-        lev = level -> SetItemLevel (x::l,lev)
-      | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
-      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev)
-      | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None)
-      | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
-    ] ]
-  ;
-  syntax_extension_type:
-    [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
-      | IDENT "bigint" -> ETBigint
-      | IDENT "binder" -> ETBinder true
-      | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n)
-      | IDENT "pattern" -> ETPattern (false,None)
-      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n)
-      | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None)
-      | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n)
-      | IDENT "closed"; IDENT "binder" -> ETBinder false
-    ] ]
-  ;
-  at_level:
-    [ [ "at"; n = level -> n ] ]
-  ;
-  constr_as_binder_kind:
-    [ [ "as"; IDENT "ident" -> AsIdent
-      | "as"; IDENT "pattern" -> AsIdentOrPattern
-      | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ]
-  ;
-END
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 103e1188a9..da4a0421b7 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,11 +1,6 @@
 Tok
 CLexer
 Extend
-Vernacexpr
 Pcoq
-Egramml
-Egramcoq
 G_constr
-G_vernac
 G_prim
-G_proofs
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 258c4bb11c..b78c35c26f 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -145,7 +145,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
 
 end
 
-
 let warning_verbose = Gramext.warning_verbose
 
 let of_coq_assoc = function
@@ -387,7 +386,6 @@ let create_universe 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
@@ -493,44 +491,6 @@ module Module =
     let module_type = Gram.entry_create "module_type"
   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_control = gec_vernac "Vernac.vernac_control"
-    let rec_definition = gec_vernac "Vernac.rec_definition"
-    let red_expr = make_gen_entry utactic "red_expr"
-    let hint_info = gec_vernac "hint_info"
-    (* Main vernac entry *)
-    let main_entry = Gram.entry_create "vernac"
-    let noedit_mode = gec_vernac "noedit_command"
-
-    let () =
-      let act_vernac = Gram.action (fun v loc -> Some (to_coqloc 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_control) ], act_vernac );
-      ] in
-      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
@@ -635,7 +595,6 @@ let () =
   Grammar.register0 wit_ref (Prim.reference);
   Grammar.register0 wit_sort_family (Constr.sort_family);
   Grammar.register0 wit_constr (Constr.constr);
-  Grammar.register0 wit_red_expr (Vernac_.red_expr);
   ()
 
 (** Registering extra grammar *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 387a62604f..36e5e420ac 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -10,12 +10,10 @@
 
 open Names
 open Extend
-open Vernacexpr
 open Genarg
 open Constrexpr
 open Libnames
 open Misctypes
-open Genredexpr
 
 (** The parser of Coq *)
 
@@ -89,6 +87,12 @@ module type S =
 
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
+module Symbols : sig
+
+  val stoken : Tok.t -> Gram.symbol
+  val snterm : Gram.internal_entry -> Gram.symbol
+end
+
 (** The parser of Coq is built from three kinds of rule declarations:
 
    - dynamic rules declared at the evaluation of Coq files (using
@@ -177,11 +181,14 @@ val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
 type gram_universe
 
 val get_univ : string -> gram_universe
+val create_universe : string -> gram_universe
+
+val new_entry : gram_universe -> string -> 'a Gram.entry
 
 val uprim : gram_universe
 val uconstr : gram_universe
 val utactic : gram_universe
-val uvernac : gram_universe
+
 
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
@@ -249,27 +256,6 @@ module Module :
     val module_type : module_ast Gram.entry
   end
 
-module Vernac_ :
-  sig
-    val gallina : vernac_expr Gram.entry
-    val gallina_ext : vernac_expr Gram.entry
-    val command : vernac_expr Gram.entry
-    val syntax : vernac_expr Gram.entry
-    val vernac_control : vernac_control Gram.entry
-    val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val noedit_mode : vernac_expr Gram.entry
-    val command_entry : vernac_expr Gram.entry
-    val red_expr : raw_red_expr Gram.entry
-    val hint_info : Typeclasses.hint_info_expr Gram.entry
-  end
-
-(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Gram.entry
-
-(** 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 epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** {5 Extending the parser without synchronization} *)
diff --git a/parsing/vernacexpr.ml b/parsing/vernacexpr.ml
deleted file mode 100644
index 6ebf66349c..0000000000
--- a/parsing/vernacexpr.ml
+++ /dev/null
@@ -1,530 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Misctypes
-open Constrexpr
-open Libnames
-
-(** Vernac expressions, produced by the parser *)
-type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
-
-type goal_selector = Goal_select.t =
-  | SelectAlreadyFocused
-  | SelectNth of int
-  | SelectList of (int * int) list
-  | SelectId of Id.t
-  | SelectAll
-[@@ocaml.deprecated "Use Goal_select.t"]
-
-type goal_identifier = string
-type scope_name = string
-
-type goal_reference =
-  | OpenSubgoals
-  | NthGoal of int
-  | GoalId of Id.t
-
-type univ_name_list = UnivNames.univ_name_list
-[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
-
-type printable =
-  | PrintTables
-  | PrintFullContext
-  | PrintSectionContext of reference
-  | PrintInspect of int
-  | PrintGrammar of string
-  | PrintLoadPath of DirPath.t option
-  | PrintModules
-  | PrintModule of reference
-  | PrintModuleType of reference
-  | PrintNamespace of DirPath.t
-  | PrintMLLoadPath
-  | PrintMLModules
-  | PrintDebugGC
-  | PrintName of reference or_by_notation * UnivNames.univ_name_list option
-  | PrintGraph
-  | PrintClasses
-  | PrintTypeClasses
-  | PrintInstances of reference or_by_notation
-  | PrintCoercions
-  | PrintCoercionPaths of class_rawexpr * class_rawexpr
-  | PrintCanonicalConversions
-  | PrintUniverses of bool * string option
-  | PrintHint of reference or_by_notation
-  | PrintHintGoal
-  | PrintHintDbName of string
-  | PrintHintDb
-  | PrintScopes
-  | PrintScope of string
-  | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
-  | PrintImplicit of reference or_by_notation
-  | PrintAssumptions of bool * bool * reference or_by_notation
-  | PrintStrategy of reference or_by_notation option
-
-type search_about_item =
-  | SearchSubPattern of constr_pattern_expr
-  | SearchString of string * scope_name option
-
-type searchable =
-  | SearchPattern of constr_pattern_expr
-  | SearchRewrite of constr_pattern_expr
-  | SearchHead of constr_pattern_expr
-  | SearchAbout of (bool * search_about_item) list
-
-type locatable =
-  | LocateAny of reference or_by_notation
-  | LocateTerm of reference or_by_notation
-  | LocateLibrary of reference
-  | LocateModule of reference
-  | LocateOther of string * reference
-  | LocateFile of string
-
-type showable =
-  | ShowGoal of goal_reference
-  | ShowProof
-  | ShowScript
-  | ShowExistentials
-  | ShowUniverses
-  | ShowProofNames
-  | ShowIntros of bool
-  | ShowMatch of reference
-
-type comment =
-  | CommentConstr of constr_expr
-  | CommentString of string
-  | CommentInt of int
-
-type reference_or_constr =
-  | HintsReference of reference
-  | HintsConstr of constr_expr
-
-type hint_mode =
-  | ModeInput (* No evars *)
-  | ModeNoHeadEvar (* No evar at the head *)
-  | ModeOutput (* Anything *)
-
-type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
-    { hint_priority : int option;
-      hint_pattern : 'a option }
-[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"]
-
-type hint_info_expr = Typeclasses.hint_info_expr
-[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"]
-
-type hints_expr =
-  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of reference list
-  | HintsTransparency of reference list * bool
-  | HintsMode of reference * hint_mode list
-  | HintsConstructors of reference list
-  | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
-
-type search_restriction =
-  | SearchInside of reference list
-  | SearchOutside of reference list
-
-type rec_flag       = bool (* true = Rec;           false = NoRec          *)
-type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
-type opacity_flag   = Proof_global.opacity_flag = Opaque | Transparent
- [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"]
-type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
-type instance_flag  = bool option
-  (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
-type export_flag    = bool (* true = Export;        false = Import         *)
-type inductive_flag = Declarations.recursivity_kind
-type onlyparsing_flag = Flags.compat_version option
- (* Some v = Parse only;  None = Print also.
-    If v<>Current, it contains the name of the coq version
-    which this notation is trying to be compatible with *)
-type locality_flag  = bool (* true = Local *)
-
-type option_value = Goptions.option_value =
-  | BoolValue of bool
-  | IntValue of int option
-  | StringValue of string
-  | StringOptValue of string option
-
-type option_ref_value =
-  | StringRefValue of string
-  | QualidRefValue of reference
-
-(** Identifier and optional list of bound universes and constraints. *)
-
-type sort_expr = Sorts.family
-
-type definition_expr =
-  | ProveBody of local_binder_expr list * constr_expr
-  | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
-      * constr_expr option
-
-type fixpoint_expr =
-    ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
-
-type cofixpoint_expr =
-    ident_decl * local_binder_expr list * constr_expr * constr_expr option
-
-type local_decl_expr =
-  | AssumExpr of lname * constr_expr
-  | DefExpr of lname * constr_expr * constr_expr option
-
-type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *)
-type decl_notation = lstring * constr_expr * scope_name option
-type simple_binder = lident list  * constr_expr
-type class_binder = lident * constr_expr list
-type 'a with_coercion = coercion_flag * 'a
-type 'a with_instance = instance_flag * 'a
-type 'a with_notation = 'a * decl_notation list
-type 'a with_priority = 'a * int option
-type constructor_expr = (lident * constr_expr) with_coercion
-type constructor_list_or_record_decl_expr =
-  | Constructors of constructor_expr list
-  | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
-type inductive_expr =
-  ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
-    constructor_list_or_record_decl_expr
-
-type one_inductive_expr =
-  ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
-
-type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
-and typeclass_context = typeclass_constraint list
-
-type proof_expr =
-  ident_decl * (local_binder_expr list * constr_expr)
-
-type syntax_modifier =
-  | SetItemLevel of string list * Extend.production_level
-  | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option
-  | SetLevel of int
-  | SetAssoc of Extend.gram_assoc
-  | SetEntryType of string * Extend.simple_constr_prod_entry_key
-  | SetOnlyParsing
-  | SetOnlyPrinting
-  | SetCompatVersion of Flags.compat_version
-  | SetFormat of string * lstring
-
-type proof_end =
-  | Admitted
-  (*                         name in `Save ident` when closing goal *)
-  | Proved of Proof_global.opacity_flag * lident option
-
-type scheme =
-  | InductionScheme of bool * reference or_by_notation * sort_expr
-  | CaseScheme of bool * reference or_by_notation * sort_expr
-  | EqualityScheme of reference or_by_notation
-
-type section_subset_expr =
-  | SsEmpty
-  | SsType
-  | SsSingl of lident
-  | SsCompl of section_subset_expr
-  | SsUnion of section_subset_expr * section_subset_expr
-  | SsSubstr of section_subset_expr * section_subset_expr
-  | SsFwdClose of section_subset_expr
-
-(** Extension identifiers for the VERNAC EXTEND mechanism.
-
-    {b ("Extraction", 0} indicates {b Extraction {i qualid}} command.
-
-    {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command.
-
-    {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command.
-
-    {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command.
-
-    {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command.
-
-    {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command.
-
-    {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands.
-
-    {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command.
-
-    {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command.
-
-    {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command.
-
-    {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command.
-
-    {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command.
- *)
-type extend_name =
-  (** Name of the vernac entry where the tactic is defined, typically found
-      after the VERNAC EXTEND statement in the source. *)
-  string *
-  (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
-      is given an offset, starting from zero. *)
-  int
-
-(* This type allows registering the inlining of constants in native compiler.
-   It will be extended with primitive inductive types and operators *)
-type register_kind =
-  | RegisterInline
-
-type bullet = Proof_bullet.t
-[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
-
-(** {6 Types concerning the module layer} *)
-
-(** Rigid / flexible module signature *)
-
-type 'a module_signature = 'a Declaremods.module_signature =
-  | Enforce of 'a (** ... : T *)
-  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
-[@@ocaml.deprecated "please use [Declaremods.module_signature]."]
-
-(** Which module inline annotations should we honor,
-    either None or the ones whose level is less or equal
-    to the given integer *)
-
-type inline = Declaremods.inline =
-  | NoInline
-  | DefaultInline
-  | InlineAt of int
-[@@ocaml.deprecated "please use [Declaremods.inline]."]
-
-type module_ast_inl = module_ast * Declaremods.inline
-type module_binder = bool option * lident list * module_ast_inl
-
-(** [Some b] if locally enabled/disabled according to [b], [None] if
-    we should use the global flag. *)
-type vernac_cumulative = VernacCumulative | VernacNonCumulative
-
-(** {6 The type of vernacular expressions} *)
-
-type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
-type vernac_argument_status = {
-  name : Name.t;
-  recarg_like : bool;
-  notation_scope : string CAst.t option;
-  implicit_status : vernac_implicit_status;
-}
-
-type nonrec vernac_expr =
-
-  | VernacLoad of verbose_flag * string
-  (* Syntax *)
-  | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
-  | VernacOpenCloseScope of bool * scope_name
-  | VernacDelimiters of scope_name * string option
-  | VernacBindScope of scope_name * class_rawexpr list
-  | VernacInfix of (lstring * syntax_modifier list) *
-      constr_expr * scope_name option
-  | VernacNotation of
-      constr_expr * (lstring * syntax_modifier list) *
-      scope_name option
-  | VernacNotationAddFormat of string * string * string
-
-  (* Gallina *)
-  | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
-  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
-  | VernacEndProof of proof_end
-  | VernacExactProof of constr_expr
-  | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
-      Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
-  | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
-  | VernacScheme of (lident option * scheme) list
-  | VernacCombinedScheme of lident * lident list
-  | VernacUniverse of lident list
-  | VernacConstraint of Glob_term.glob_constraint list
-
-  (* Gallina extensions *)
-  | VernacBeginSection of lident
-  | VernacEndSegment of lident
-  | VernacRequire of
-      reference option * export_flag option * reference list
-  | VernacImport of export_flag * reference list
-  | VernacCanonical of reference or_by_notation
-  | VernacCoercion of reference or_by_notation *
-      class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
-  | VernacNameSectionHypSet of lident * section_subset_expr
-
-  (* Type classes *)
-  | VernacInstance of
-      bool * (* abstract instance *)
-      local_binder_expr list * (* super *)
-        typeclass_constraint * (* instance name, class name, params *)
-        (bool * constr_expr) option * (* props *)
-        Typeclasses.hint_info_expr
-
-  | VernacContext of local_binder_expr list
-
-  | VernacDeclareInstances of
-    (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *)
-
-  | VernacDeclareClass of reference (* inductive or definition name *)
-
-  (* Modules and Module Types *)
-  | VernacDeclareModule of bool option * lident *
-      module_binder list * module_ast_inl
-  | VernacDefineModule of bool option * lident * module_binder list *
-      module_ast_inl Declaremods.module_signature * module_ast_inl list
-  | VernacDeclareModuleType of lident *
-      module_binder list * module_ast_inl list * module_ast_inl list
-  | VernacInclude of module_ast_inl list
-
-  (* Solving *)
-
-  | VernacSolveExistential of int * constr_expr
-
-  (* Auxiliary file and library management *)
-  | VernacAddLoadPath of rec_flag * string * DirPath.t option
-  | VernacRemoveLoadPath of string
-  | VernacAddMLPath of rec_flag * string
-  | VernacDeclareMLModule of string list
-  | VernacChdir of string option
-
-  (* State management *)
-  | VernacWriteState of string
-  | VernacRestoreState of string
-
-  (* Resetting *)
-  | VernacResetName of lident
-  | VernacResetInitial
-  | VernacBack of int
-  | VernacBackTo of int
-
-  (* Commands *)
-  | VernacCreateHintDb of string * bool
-  | VernacRemoveHints of string list * reference list
-  | VernacHints of string list * hints_expr
-  | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
-      onlyparsing_flag
-  | VernacArguments of reference or_by_notation *
-      vernac_argument_status list (* Main arguments status list *) *
-        (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
-      int option (* Number of args to trigger reduction *) *
-        [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
-          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
-          `DefaultImplicits ] list
-  | VernacReserve of simple_binder list
-  | VernacGeneralizable of (lident list) option
-  | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
-  | VernacSetStrategy of
-      (Conv_oracle.level * reference or_by_notation list) list
-  | VernacUnsetOption of export_flag * Goptions.option_name
-  | VernacSetOption of export_flag * Goptions.option_name * option_value
-  | VernacAddOption of Goptions.option_name * option_ref_value list
-  | VernacRemoveOption of Goptions.option_name * option_ref_value list
-  | VernacMemOption of Goptions.option_name * option_ref_value list
-  | VernacPrintOption of Goptions.option_name
-  | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
-  | VernacGlobalCheck of constr_expr
-  | VernacDeclareReduction of string * Genredexpr.raw_red_expr
-  | VernacPrint of printable
-  | VernacSearch of searchable * Goal_select.t option * search_restriction
-  | VernacLocate of locatable
-  | VernacRegister of lident * register_kind
-  | VernacComments of comment list
-
-  (* Proof management *)
-  | VernacAbort of lident option
-  | VernacAbortAll
-  | VernacRestart
-  | VernacUndo of int
-  | VernacUndoTo of int
-  | VernacFocus of int option
-  | VernacUnfocus
-  | VernacUnfocused
-  | VernacBullet of Proof_bullet.t
-  | VernacSubproof of Goal_select.t option
-  | VernacEndSubproof
-  | VernacShow of showable
-  | VernacCheckGuard
-  | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
-  | VernacProofMode of string
-
-  (* For extension *)
-  | VernacExtend of extend_name * Genarg.raw_generic_argument list
-
-type nonrec vernac_flag =
-  | VernacProgram
-  | VernacPolymorphic of bool
-  | VernacLocal of bool
-
-type vernac_control =
-  | VernacExpr of vernac_flag list * vernac_expr
-  (* boolean is true when the `-time` batch-mode command line flag was set.
-     the flag is used to print differently in `-time` vs `Time foo` *)
-  | VernacTime of bool * vernac_control CAst.t
-  | VernacRedirect of string * vernac_control CAst.t
-  | VernacTimeout of int * vernac_control
-  | VernacFail of vernac_control
-
-(* A vernac classifier provides information about the exectuion of a
-   command:
-
-   - vernac_when: encodes if the vernac may alter the parser [thus
-     forcing immediate execution], or if indeed it is pure and parsing
-     can continue without its execution.
-
-   - vernac_type: if it is starts, ends, continues a proof or
-     alters the global state or is a control command like BackTo or is
-     a query like Check.
-
-   The classification works on the assumption that we have 3 states:
-   parsing, execution (global enviroment, etc...), and proof
-   state. For example, commands that only alter the proof state are
-   considered safe to delegate to a worker.
-
-*)
-type vernac_type =
-  (* Start of a proof *)
-  | VtStartProof of vernac_start
-  (* Command altering the global state, bad for parallel
-     processing. *)
-  | VtSideff of vernac_sideff_type
-  (* End of a proof *)
-  | VtQed of vernac_qed_type
-  (* A proof step *)
-  | VtProofStep of proof_step
-  (* To be removed *)
-  | VtProofMode of string
-  (* Queries are commands assumed to be "pure", that is to say, they
-     don't modify the interpretation state. *)
-  | VtQuery
-  (* To be removed *)
-  | VtMeta
-  | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
-and vernac_start = string * opacity_guarantee * Id.t list
-and vernac_sideff_type = Id.t list
-and opacity_guarantee =
-  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
-  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
-and proof_step = { (* TODO: inline with OCaml 4.03 *)
-  parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
-  proof_block_detection : proof_block_name option
-}
-and solving_tac = bool (* a terminator *)
-and anon_abstracting_tac = bool (* abstracting anonymously its result *)
-and proof_block_name = string (* open type of delimiters *)
-type vernac_when =
-  | VtNow
-  | VtLater
-type vernac_classification = vernac_type * vernac_when
-
-
-(** Deprecated stuff *)
-type universe_decl_expr = Constrexpr.universe_decl_expr
-[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"]
-
-type ident_decl = Constrexpr.ident_decl
-[@@ocaml.deprecated "alias of Constrexpr.ident_decl"]
-
-type name_decl = Constrexpr.name_decl
-[@@ocaml.deprecated "alias of Constrexpr.name_decl"]