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

16 files changed, 3798 insertions, 14 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index d99d45313..40001c0a3 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -41,7 +41,7 @@ let _ = Goptions.declare_bool_option {
 let typeclasses_db = "typeclass_instances"
 
 let set_typeclass_transparency c local b = 
-  Hints.add_hints local [typeclasses_db] 
+  Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry ([c], b))
     
 let _ =
@@ -56,7 +56,7 @@ let _ =
                      (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
 		     info.hint_pattern } in
      Flags.silently (fun () ->
-	Hints.add_hints local [typeclasses_db]
+       Hints.add_hints ~local [typeclasses_db]
 	  (Hints.HintsResolveEntry
 	     [info, poly, false, Hints.PathHints path, inst'])) ());
   Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
new file mode 100644
index 000000000..5f63d21c4
--- /dev/null
+++ b/vernac/egramcoq.ml
@@ -0,0 +1,483 @@
+(************************************************************************)
+(*         *   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/vernac/egramcoq.mli b/vernac/egramcoq.mli
new file mode 100644
index 000000000..e15add10f
--- /dev/null
+++ b/vernac/egramcoq.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*         *   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/vernac/egramml.ml b/vernac/egramml.ml
new file mode 100644
index 000000000..048d4d93a
--- /dev/null
+++ b/vernac/egramml.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*         *   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 Pvernac.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/vernac/egramml.mli b/vernac/egramml.mli
new file mode 100644
index 000000000..31aa1a989
--- /dev/null
+++ b/vernac/egramml.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   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/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4
new file mode 100644
index 000000000..56229c765
--- /dev/null
+++ b/vernac/g_proofs.ml4
@@ -0,0 +1,134 @@
+(************************************************************************)
+(*         *   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 Pvernac.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/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
new file mode 100644
index 000000000..6c7df8cfa
--- /dev/null
+++ b/vernac/g_vernac.ml4
@@ -0,0 +1,1154 @@
+(************************************************************************)
+(*         *   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.Module
+open Pvernac.Vernac_
+
+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/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 76958b05f..e038f54dd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -76,15 +76,15 @@ let pr_grammar = function
       pr_entry Pcoq.Constr.pattern
   | "vernac" ->
       str "Entry vernac_control is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.vernac_control ++
+      pr_entry Pvernac.Vernac_.vernac_control ++
       str "Entry command is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.command ++
+      pr_entry Pvernac.Vernac_.command ++
       str "Entry syntax is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.syntax ++
+      pr_entry Pvernac.Vernac_.syntax ++
       str "Entry gallina is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.gallina ++
+      pr_entry Pvernac.Vernac_.gallina ++
       str "Entry gallina_ext is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.gallina_ext
+      pr_entry Pvernac.Vernac_.gallina_ext
   | name -> pr_registered_grammar name
 
 (**********************************************************************)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index dfc51a990..6ef8294df 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -616,7 +616,7 @@ let shrink_body c ty =
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_hint local prg cst =
-  Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+  Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
 
 let it_mkLambda_or_LetIn_or_clean t ctx =
   let open Context.Rel.Declaration in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
new file mode 100644
index 000000000..3655947a5
--- /dev/null
+++ b/vernac/ppvernac.ml
@@ -0,0 +1,1219 @@
+(************************************************************************)
+(*         *   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 Names
+
+open CErrors
+open Util
+open CAst
+
+open Extend
+open Libnames
+open Decl_kinds
+open Constrexpr
+open Constrexpr_ops
+open Vernacexpr
+open Declaremods
+open Pputils
+
+  open Ppconstr
+
+  let do_not_tag _ x = x
+  let tag_keyword = do_not_tag ()
+  let tag_vernac  = do_not_tag
+
+  let keyword s = tag_keyword (str s)
+
+  let pr_constr = pr_constr_expr
+  let pr_lconstr = pr_lconstr_expr
+  let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
+
+  let pr_uconstraint (l, d, r) =
+    pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+      pr_glob_level r
+
+  let pr_univ_name_list = function
+    | None -> mt ()
+    | Some l ->
+      str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
+
+  let pr_univdecl_instance l extensible =
+    prlist_with_sep spc pr_lident l ++
+    (if extensible then str"+" else mt ())
+
+  let pr_univdecl_constraints l extensible =
+    if List.is_empty l && extensible then mt ()
+    else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
+           (if extensible then str"+" else mt())
+
+  let pr_universe_decl l =
+    let open Misctypes in
+    match l with
+    | None -> mt ()
+    | Some l ->
+      str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+        pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+
+  let pr_ident_decl (lid, l) =
+    pr_lident lid ++ pr_universe_decl l
+
+  let string_of_fqid fqid =
+    String.concat "." (List.map Id.to_string fqid)
+
+  let pr_fqid fqid = str (string_of_fqid fqid)
+
+  let pr_lfqid {CAst.loc;v=fqid} =
+    match loc with
+    | None     -> pr_fqid fqid
+    | Some loc -> let (b,_) = Loc.unloc loc in
+                  pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid
+
+  let pr_lname_decl (n, u) =
+    pr_lname n ++ pr_universe_decl u
+
+  let pr_smart_global = Pputils.pr_or_by_notation pr_reference
+
+  let pr_ltac_ref = Libnames.pr_reference
+
+  let pr_module = Libnames.pr_reference
+
+  let pr_import_module = Libnames.pr_reference
+
+  let sep_end = function
+    | VernacBullet _
+    | VernacSubproof _
+    | VernacEndSubproof -> str""
+    | _ -> str"."
+
+  let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t
+
+  let sep = fun _ -> spc()
+  let sep_v2 = fun _ -> str"," ++ spc()
+
+  let pr_at_level = function
+    | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+    | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+
+  let pr_constr_as_binder_kind = function
+    | AsIdent -> keyword "as ident"
+    | AsIdentOrPattern -> keyword "as pattern"
+    | AsStrictPattern -> keyword "as strict pattern"
+
+  let pr_strict b = if b then str "strict " else mt ()
+
+  let pr_set_entry_type pr = function
+    | ETName -> str"ident"
+    | ETReference -> str"global"
+    | ETPattern (b,None) -> pr_strict b ++ str"pattern"
+    | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+    | ETConstr lev -> str"constr" ++ pr lev
+    | ETOther (_,e) -> str e
+    | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk
+    | ETBigint -> str "bigint"
+    | ETBinder true -> str "binder"
+    | ETBinder false -> str "closed binder"
+
+  let pr_at_level_opt = function
+    | None -> mt ()
+    | Some n -> spc () ++ pr_at_level n
+
+  let pr_set_simple_entry_type =
+    pr_set_entry_type pr_at_level_opt
+
+  let pr_comment pr_c = function
+    | CommentConstr c -> pr_c c
+    | CommentString s -> qs s
+    | CommentInt n -> int n
+
+  let pr_in_out_modules = function
+    | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l
+    | SearchOutside [] -> mt()
+    | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l
+
+  let pr_search_about (b,c) =
+    (if b then str "-" else mt()) ++
+      match c with
+        | SearchSubPattern p -> pr_constr_pattern_expr p
+        | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+  let pr_search a gopt b pr_p =
+    pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
+    ++
+      match a with
+      | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchAbout sl ->
+         keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
+
+  let pr_locality local = if local then keyword "Local" else keyword "Global"
+
+  let pr_option_ref_value = function
+    | QualidRefValue id -> pr_reference id
+    | StringRefValue s -> qs s
+
+  let pr_printoption table b =
+    prlist_with_sep spc str table ++
+      pr_opt (prlist_with_sep sep pr_option_ref_value) b
+
+  let pr_set_option a b =
+    let pr_opt_value = function
+      | IntValue None -> assert false
+    (* This should not happen because of the grammar *)
+      | IntValue (Some n) -> spc() ++ int n
+      | StringValue s -> spc() ++ str s
+      | StringOptValue None -> mt()
+      | StringOptValue (Some s) -> spc() ++ str s
+      | BoolValue b -> mt()
+    in pr_printoption a None ++ pr_opt_value b
+
+  let pr_opt_hintbases l = match l with
+    | [] -> mt()
+    | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
+
+  let pr_reference_or_constr pr_c = function
+    | HintsReference r -> pr_reference r
+    | HintsConstr c -> pr_c c
+
+  let pr_hint_mode = function
+    | ModeInput -> str"+"
+    | ModeNoHeadEvar -> str"!"
+    | ModeOutput -> str"-"
+
+  let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
+    pr_opt (fun x -> str"|" ++ int x) pri ++
+    pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
+
+  let pr_hints db h pr_c pr_pat =
+    let opth = pr_opt_hintbases db  in
+    let pph =
+      match h with
+        | HintsResolve l ->
+          keyword "Resolve " ++ prlist_with_sep sep
+            (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
+            l
+        | HintsImmediate l ->
+          keyword "Immediate" ++ spc() ++
+            prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
+        | HintsUnfold l ->
+          keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l
+        | HintsTransparency (l, b) ->
+          keyword (if b then "Transparent" else "Opaque")
+          ++ spc ()
+          ++ prlist_with_sep sep pr_reference l
+        | HintsMode (m, l) ->
+          keyword "Mode"
+          ++ spc ()
+          ++ pr_reference m ++ spc() ++
+            prlist_with_sep spc pr_hint_mode l
+        | HintsConstructors c ->
+          keyword "Constructors"
+          ++ spc() ++ prlist_with_sep spc pr_reference c
+        | HintsExtern (n,c,tac) ->
+          let pat = match c with None -> mt () | Some pat -> pr_pat pat in
+          keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
+            spc() ++ Pputils.pr_raw_generic (Global.env ()) tac
+    in
+    hov 2 (keyword "Hint "++ pph ++ opth)
+
+  let pr_with_declaration pr_c = function
+    | CWith_Definition (id,udecl,c) ->
+      let p = pr_c c in
+      keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
+    | CWith_Module (id,qid) ->
+      keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
+        pr_ast pr_qualid qid
+
+  let rec pr_module_ast leading_space pr_c = function
+    | { loc ; v = CMident qid } ->
+      if leading_space then
+        spc () ++ pr_located pr_qualid (loc, qid)
+      else
+        pr_located pr_qualid (loc,qid)
+    | { v = CMwith (mty,decl) } ->
+      let m = pr_module_ast leading_space pr_c mty in
+      let p = pr_with_declaration pr_c decl in
+      m ++ spc() ++ keyword "with" ++ spc() ++ p
+    | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } ->
+      pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
+    | { v = CMapply (me1,me2) } ->
+      pr_module_ast leading_space pr_c me1 ++ spc() ++
+        hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")
+
+  let pr_inline = function
+    | DefaultInline -> mt ()
+    | NoInline -> str "[no inline]"
+    | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
+
+  let pr_assumption_inline = function
+    | DefaultInline -> str "Inline"
+    | NoInline -> mt ()
+    | InlineAt i -> str "Inline(" ++ int i ++ str ")"
+
+  let pr_module_ast_inl leading_space pr_c (mast,inl) =
+    pr_module_ast leading_space pr_c mast ++ pr_inline inl
+
+  let pr_of_module_type prc = function
+    | Enforce mty -> str ":" ++ pr_module_ast_inl true prc mty
+    | Check mtys ->
+      prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl true prc m) mtys
+
+  let pr_require_token = function
+    | Some true ->
+      keyword "Export" ++ spc ()
+    | Some false ->
+      keyword "Import" ++ spc ()
+    | None -> mt()
+
+  let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
+    let m = pr_module_ast true pr_c mty in
+    spc() ++
+      hov 1 (str"(" ++ pr_require_token export ++
+               prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
+
+  let pr_module_binders l pr_c =
+    prlist_strict (pr_module_vardecls pr_c) l
+
+  let pr_type_option pr_c = function
+    | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
+    | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
+
+  let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
+    fnl () ++ keyword "where " ++ qs ntn ++ str " := "
+    ++ Flags.without_option Flags.beautify prc c ++
+      pr_opt (fun sc -> str ": " ++ str sc) scopt
+
+  let pr_binders_arg =
+    pr_non_empty_arg pr_binders
+
+  let pr_and_type_binders_arg bl =
+    pr_binders_arg bl
+
+  let pr_onescheme (idop,schem) =
+    match schem with
+      | InductionScheme (dep,ind,s) ->
+        (match idop with
+          | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+          | None -> spc ()
+        ) ++
+          hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for")
+                 ++ spc() ++ pr_smart_global ind) ++ spc() ++
+          hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
+      | CaseScheme (dep,ind,s) ->
+        (match idop with
+          | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+          | None -> spc ()
+        ) ++
+          hov 0 ((if dep then keyword "Elimination for" else keyword "Case for")
+                 ++ spc() ++ pr_smart_global ind) ++ spc() ++
+          hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
+      | EqualityScheme ind ->
+        (match idop with
+          | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+          | None -> spc()
+        ) ++
+          hov 0 (keyword "Equality for")
+        ++ spc() ++ pr_smart_global ind
+
+  let begin_of_inductive = function
+    | [] -> 0
+    | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
+
+  let pr_class_rawexpr = function
+    | FunClass -> keyword "Funclass"
+    | SortClass -> keyword "Sortclass"
+    | RefClass qid -> pr_smart_global qid
+
+  let pr_assumption_token many discharge kind =
+    match discharge, kind with
+      | (NoDischarge,Logical) ->
+        keyword (if many then "Axioms" else "Axiom")
+      | (NoDischarge,Definitional) ->
+        keyword (if many then "Parameters" else "Parameter")
+      | (NoDischarge,Conjectural) -> str"Conjecture"
+      | (DoDischarge,Logical) ->
+        keyword (if many then "Hypotheses" else "Hypothesis")
+      | (DoDischarge,Definitional) ->
+        keyword (if many then "Variables" else "Variable")
+      | (DoDischarge,Conjectural) ->
+        anomaly (Pp.str "Don't know how to beautify a local conjecture.")
+
+  let pr_params pr_c (xl,(c,t)) =
+    hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
+             (if c then str":>" else str":" ++
+                 spc() ++ pr_c t))
+
+  let rec factorize = function
+    | [] -> []
+    | (c,(idl,t))::l ->
+      match factorize l with
+        | (xl,((c', t') as r))::l'
+            when (c : bool) == c' && Pervasives.(=) t t' ->
+          (** FIXME: we need equality on constr_expr *)
+          (idl@xl,r)::l'
+        | l' -> (idl,(c,t))::l'
+
+  let pr_ne_params_list pr_c l =
+    match factorize l with
+      | [p] -> pr_params pr_c p
+      | l ->
+        prlist_with_sep spc
+          (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+
+(*
+  prlist_with_sep pr_semicolon (pr_params pr_c)
+*)
+
+  let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
+
+  let pr_syntax_modifier = function
+    | SetItemLevel (l,n) ->
+      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
+    | SetItemLevelAsBinder (l,bk,n) ->
+      prlist_with_sep sep_v2 str l ++
+      spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk
+    | SetLevel n -> pr_at_level (NumLevel n)
+    | SetAssoc LeftA -> keyword "left associativity"
+    | SetAssoc RightA -> keyword "right associativity"
+    | SetAssoc NonA -> keyword "no associativity"
+    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
+    | SetOnlyPrinting -> keyword "only printing"
+    | SetOnlyParsing -> keyword "only parsing"
+    | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
+    | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
+    | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
+
+  let pr_syntax_modifiers = function
+    | [] -> mt()
+    | l -> spc() ++
+      hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+
+  let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) =
+    let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
+    let annot = pr_guard_annot pr_lconstr_expr bl ro in
+    pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot
+    ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
+    ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
+    ++ prlist (pr_decl_notation pr_constr) ntn
+
+  let pr_statement head (idpl,(bl,c)) =
+    hov 2
+      (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
+         (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+         str":" ++ pr_spc_lconstr c)
+
+(**************************************)
+(* Pretty printer for vernac commands *)
+(**************************************)
+
+  let pr_constrarg c = spc () ++ pr_constr c
+  let pr_lconstrarg c = spc () ++ pr_lconstr c
+  let pr_intarg n = spc () ++ int n
+
+  let pr_oc = function
+    | None -> str" :"
+    | Some true -> str" :>"
+    | Some false -> str" :>>"
+
+  let pr_record_field ((x, pri), ntn) =
+    let prx = match x with
+      | (oc,AssumExpr (id,t)) ->
+        hov 1 (pr_lname id ++
+                 pr_oc oc ++ spc() ++
+                 pr_lconstr_expr t)
+      | (oc,DefExpr(id,b,opt)) -> (match opt with
+          | Some t ->
+            hov 1 (pr_lname id ++
+                     pr_oc oc ++ spc() ++
+                     pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+          | None ->
+            hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+                     pr_lconstr b)) in
+    let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
+    prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
+
+  let pr_record_decl b c fs =
+    pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
+      hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+
+  let pr_printable = function
+    | PrintFullContext ->
+      keyword "Print All"
+    | PrintSectionContext s ->
+      keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
+    | PrintGrammar ent ->
+      keyword "Print Grammar" ++ spc() ++ str ent
+    | PrintLoadPath dir ->
+      keyword "Print LoadPath" ++ pr_opt DirPath.print dir
+    | PrintModules ->
+      keyword "Print Modules"
+    | PrintMLLoadPath ->
+      keyword "Print ML Path"
+    | PrintMLModules ->
+      keyword "Print ML Modules"
+    | PrintDebugGC ->
+      keyword "Print ML GC"
+    | PrintGraph ->
+      keyword "Print Graph"
+    | PrintClasses ->
+      keyword "Print Classes"
+    | PrintTypeClasses ->
+      keyword "Print TypeClasses"
+    | PrintInstances qid ->
+      keyword "Print Instances" ++ spc () ++ pr_smart_global qid
+    | PrintCoercions ->
+      keyword "Print Coercions"
+    | PrintCoercionPaths (s,t) ->
+      keyword "Print Coercion Paths" ++ spc()
+      ++ pr_class_rawexpr s ++ spc()
+      ++ pr_class_rawexpr t
+    | PrintCanonicalConversions ->
+      keyword "Print Canonical Structures"
+    | PrintTables ->
+      keyword "Print Tables"
+    | PrintHintGoal ->
+      keyword "Print Hint"
+    | PrintHint qid ->
+      keyword "Print Hint" ++ spc () ++ pr_smart_global qid
+    | PrintHintDb ->
+      keyword "Print Hint *"
+    | PrintHintDbName s ->
+      keyword "Print HintDb" ++ spc () ++ str s
+    | PrintUniverses (b, fopt) ->
+      let cmd =
+        if b then "Print Sorted Universes"
+        else "Print Universes"
+      in
+      keyword cmd ++ pr_opt str fopt
+    | PrintName (qid,udecl) ->
+      keyword "Print" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list udecl
+    | PrintModuleType qid ->
+      keyword "Print Module Type" ++ spc() ++ pr_reference qid
+    | PrintModule qid ->
+      keyword "Print Module" ++ spc() ++ pr_reference qid
+    | PrintInspect n ->
+      keyword "Inspect" ++ spc() ++ int n
+    | PrintScopes ->
+      keyword "Print Scopes"
+    | PrintScope s ->
+      keyword "Print Scope" ++ spc() ++ str s
+    | PrintVisibility s ->
+      keyword "Print Visibility" ++ pr_opt str s
+    | PrintAbout (qid,l,gopt) ->
+       pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
+       ++ keyword "About" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list l
+    | PrintImplicit qid ->
+      keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
+    (* spiwack: command printing all the axioms and section variables used in a
+       term *)
+    | PrintAssumptions (b, t, qid) ->
+      let cmd = match b, t with
+        | true, true -> "Print All Dependencies"
+        | true, false -> "Print Opaque Dependencies"
+        | false, true -> "Print Transparent Dependencies"
+        | false, false -> "Print Assumptions"
+      in
+      keyword cmd ++ spc() ++ pr_smart_global qid
+    | PrintNamespace dp ->
+      keyword "Print Namespace" ++ DirPath.print dp
+    | PrintStrategy None ->
+      keyword "Print Strategies"
+    | PrintStrategy (Some qid) ->
+      keyword "Print Strategy" ++ pr_smart_global qid
+
+  let pr_using e =
+    let rec aux = function
+      | SsEmpty -> "()"
+      | SsType -> "(Type)"
+      | SsSingl { v=id } -> "("^Id.to_string id^")"
+      | SsCompl e -> "-" ^ aux e^""
+      | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
+      | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
+      | SsFwdClose e -> "("^aux e^")*"
+    in Pp.str (aux e)
+
+  let pr_extend s cl =
+    let pr_arg a =
+      try pr_gen a
+      with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
+    try
+      let rl = Egramml.get_extend_vernac_rule s in
+      let rec aux rl cl =
+        match rl, cl with
+        | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+        | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+        | [], [] -> []
+        | _ -> assert false in
+      hov 1 (pr_sequence identity (aux rl cl))
+    with Not_found ->
+      hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+  let pr_vernac_expr v =
+    let return = tag_vernac v in
+    match v with
+      | VernacLoad (f,s) ->
+        return (
+          keyword "Load"
+          ++ if f then
+              (spc() ++ keyword "Verbose" ++ spc())
+            else
+              spc() ++ qs s
+        )
+
+      (* Proof management *)
+      | VernacAbortAll ->
+        return (keyword "Abort All")
+      | VernacRestart ->
+        return (keyword "Restart")
+      | VernacUnfocus ->
+        return (keyword "Unfocus")
+      | VernacUnfocused ->
+        return (keyword "Unfocused")
+      | VernacAbort id ->
+        return (keyword "Abort" ++ pr_opt pr_lident id)
+      | VernacUndo i ->
+        return (
+          if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i
+        )
+      | VernacUndoTo i ->
+        return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
+      | VernacFocus i ->
+        return (keyword "Focus" ++ pr_opt int i)
+      | VernacShow s ->
+        let pr_goal_reference = function
+          | OpenSubgoals -> mt ()
+          | NthGoal n -> spc () ++ int n
+          | GoalId id -> spc () ++ pr_id id
+        in
+        let pr_showable = function
+          | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
+          | ShowProof -> keyword "Show Proof"
+          | ShowScript -> keyword "Show Script"
+          | ShowExistentials -> keyword "Show Existentials"
+          | ShowUniverses -> keyword "Show Universes"
+          | ShowProofNames -> keyword "Show Conjectures"
+          | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
+          | ShowMatch id -> keyword "Show Match " ++ pr_reference id
+        in
+        return (pr_showable s)
+      | VernacCheckGuard ->
+        return (keyword "Guarded")
+
+    (* Resetting *)
+      | VernacResetName id ->
+        return (keyword "Reset" ++ spc() ++ pr_lident id)
+      | VernacResetInitial ->
+        return (keyword "Reset Initial")
+      | VernacBack i ->
+        return (
+          if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
+        )
+      | VernacBackTo i ->
+        return (keyword "BackTo" ++ pr_intarg i)
+
+    (* State management *)
+      | VernacWriteState s ->
+        return (keyword "Write State" ++ spc () ++ qs s)
+      | VernacRestoreState s ->
+        return  (keyword "Restore State" ++ spc() ++ qs s)
+
+    (* Syntax *)
+      | VernacOpenCloseScope (opening,sc) ->
+        return (
+          keyword (if opening then "Open " else "Close ") ++
+            keyword "Scope" ++ spc() ++ str sc
+        )
+      | VernacDelimiters (sc,Some key) ->
+        return (
+          keyword "Delimit Scope" ++ spc () ++ str sc ++
+            spc() ++ keyword "with" ++ spc () ++ str key
+        )
+      | VernacDelimiters (sc, None) ->
+        return (
+          keyword "Undelimit Scope" ++ spc () ++ str sc
+        )
+      | VernacBindScope (sc,cll) ->
+        return (
+          keyword "Bind Scope" ++ spc () ++ str sc ++
+            spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
+        )
+      | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *)
+        return (
+          hov 0 (hov 0 (keyword "Infix "
+                        ++ qs s ++ str " :=" ++ pr_constrarg q) ++
+                   pr_syntax_modifiers mv ++
+                   (match sn with
+                     | None -> mt()
+                     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+        )
+      | VernacNotation (c,({v=s},l),opt) ->
+        return (
+          hov 2 (keyword "Notation" ++ spc() ++ qs s ++
+                   str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
+                   (match opt with
+                     | None -> mt()
+                     | Some sc -> str" :" ++ spc() ++ str sc))
+        )
+      | VernacSyntaxExtension (_, (s, l)) ->
+        return (
+          keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++
+            pr_syntax_modifiers l
+        )
+      | VernacNotationAddFormat(s,k,v) ->
+        return (
+          keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
+        )
+
+      (* Gallina *)
+      | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
+        let pr_def_token dk =
+          keyword (
+            if Name.is_anonymous (fst id).v
+            then "Goal"
+            else Kindops.string_of_definition_object_kind dk)
+        in
+        let pr_reduce = function
+          | None -> mt()
+          | Some r ->
+            keyword "Eval" ++ spc() ++
+              pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
+              keyword " in" ++ spc()
+        in
+        let pr_def_body = function
+          | DefineBody (bl,red,body,d) ->
+            let ty = match d with
+              | None -> mt()
+              | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
+            in
+            (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
+          | ProveBody (bl,t) ->
+            let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
+            (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
+        let (binds,typ,c) = pr_def_body b in
+        return (
+          hov 2 (
+            pr_def_token kind ++ spc()
+            ++ pr_lname_decl id ++ binds ++ typ
+            ++ (match c with
+              | None -> mt()
+              | Some cc -> str" :=" ++ spc() ++ cc))
+        )
+
+      | VernacStartTheoremProof (ki,l) ->
+        return (
+          hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
+                   prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
+        )
+
+      | VernacEndProof Admitted ->
+        return (keyword "Admitted")
+
+      | VernacEndProof (Proved (opac,o)) -> return (
+        let open Proof_global in
+        match o with
+          | None -> (match opac with
+              | Transparent -> keyword "Defined"
+              | Opaque      -> keyword "Qed")
+          | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+      )
+      | VernacExactProof c ->
+        return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
+      | VernacAssumption ((discharge,kind),t,l) ->
+        let n = List.length (List.flatten (List.map fst (List.map snd l))) in
+        let pr_params (c, (xl, t)) =
+          hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
+            (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
+        let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
+        return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
+                       pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
+      | VernacInductive (cum, p,f,l) ->
+        let pr_constructor (coe,(id,c)) =
+          hov 2 (pr_lident id ++ str" " ++
+                   (if coe then str":>" else str":") ++
+                   Flags.without_option Flags.beautify pr_spc_lconstr c)
+        in
+        let pr_constructor_list b l = match l with
+          | Constructors [] -> mt()
+          | Constructors l ->
+            let fst_sep = match l with [_] -> "   " | _ -> " | " in
+            pr_com_at (begin_of_inductive l) ++
+              fnl() ++ str fst_sep ++
+              prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
+          | RecordDecl (c,fs) ->
+            pr_record_decl b c fs
+        in
+        let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) =
+          hov 0 (
+            str key ++ spc() ++
+              (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
+              pr_and_type_binders_arg indpar ++
+              pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
+              str" :=") ++ pr_constructor_list k lc ++
+            prlist (pr_decl_notation pr_constr) ntn
+        in
+        let key =
+          let (_,_,_,k,_),_ = List.hd l in
+          let kind =
+            match k with Record -> "Record" | Structure -> "Structure"
+                       | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+                       | Class _ -> "Class" | Variant -> "Variant"
+          in
+          if p then
+            let cm =
+              match cum with
+              | Some VernacCumulative -> "Cumulative"
+              | Some VernacNonCumulative -> "NonCumulative"
+              | None -> ""
+            in
+            cm ^ " " ^ kind
+          else kind
+        in
+        return (
+          hov 1 (pr_oneind key (List.hd l)) ++
+          (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+        )
+
+      | VernacFixpoint (local, recs) ->
+        let local = match local with
+          | DoDischarge -> "Let "
+          | NoDischarge -> ""
+        in
+        return (
+          hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
+                   prlist_with_sep (fun _ -> fnl () ++ keyword "with"
+                     ++ spc ()) pr_rec_definition recs)
+        )
+
+      | VernacCoFixpoint (local, corecs) ->
+        let local = match local with
+          | DoDischarge -> keyword "Let" ++ spc ()
+          | NoDischarge -> str ""
+        in
+        let pr_onecorec ((iddecl,bl,c,def),ntn) =
+          pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+            spc() ++ pr_lconstr_expr c ++
+            pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
+            prlist (pr_decl_notation pr_constr) ntn
+        in
+        return (
+          hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
+                   prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
+        )
+      | VernacScheme l ->
+        return (
+          hov 2 (keyword "Scheme" ++ spc() ++
+                   prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l)
+        )
+      | VernacCombinedScheme (id, l) ->
+        return (
+          hov 2 (keyword "Combined Scheme" ++ spc() ++
+                   pr_lident id ++ spc() ++ keyword "from" ++ spc() ++
+                   prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+        )
+      | VernacUniverse v ->
+        return (
+          hov 2 (keyword "Universe" ++ spc () ++
+                   prlist_with_sep (fun _ -> str",") pr_lident v)
+        )
+      | VernacConstraint v ->
+        return (
+          hov 2 (keyword "Constraint" ++ spc () ++
+                   prlist_with_sep (fun _ -> str",") pr_uconstraint v)
+        )
+
+      (* Gallina extensions *)
+      | VernacBeginSection id ->
+        return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
+      | VernacEndSegment id ->
+        return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
+      | VernacNameSectionHypSet (id,set) ->
+        return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
+        str ":="++spc()++pr_using set))
+      | VernacRequire (from, exp, l) ->
+        let from = match from with
+        | None -> mt ()
+        | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
+        in
+        return (
+          hov 2
+            (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
+               prlist_with_sep sep pr_module l)
+        )
+      | VernacImport (f,l) ->
+        return (
+          (if f then keyword "Export" else keyword "Import") ++ spc() ++
+            prlist_with_sep sep pr_import_module l
+        )
+      | VernacCanonical q ->
+        return (
+          keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
+        )
+      | VernacCoercion (id,c1,c2) ->
+        return (
+          hov 1 (
+            keyword "Coercion" ++ spc() ++
+              pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
+              spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
+        )
+      | VernacIdentityCoercion (id,c1,c2) ->
+        return (
+          hov 1 (
+            keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
+              spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
+              spc() ++ pr_class_rawexpr c2)
+        )
+
+      | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
+        return (
+          hov 1 (
+            (if abst then keyword "Declare" ++ spc () else mt ()) ++
+            keyword "Instance" ++
+            (match instid with
+             | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
+             | { v = Anonymous }, _ -> mt ()) ++
+            pr_and_type_binders_arg sup ++
+              str":" ++ spc () ++
+              (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
+              pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
+              (match props with
+                | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
+                | Some (true,_) -> assert false
+                | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
+                | None -> mt()))
+        )
+
+      | VernacContext l ->
+        return (
+          hov 1 (
+            keyword "Context" ++ pr_and_type_binders_arg l)
+        )
+
+      | VernacDeclareInstances insts ->
+         let pr_inst (id, info) =
+           pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+         in
+         return (
+          hov 1 (keyword "Existing" ++ spc () ++
+                   keyword(String.plural (List.length insts) "Instance") ++
+                 spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
+        )
+
+      | VernacDeclareClass id ->
+        return (
+          hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id)
+        )
+
+      (* Modules and Module Types *)
+      | VernacDefineModule (export,m,bl,tys,bd) ->
+        let b = pr_module_binders bl pr_lconstr in
+        return (
+          hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
+                   pr_lident m ++ b ++
+                   pr_of_module_type pr_lconstr tys ++
+                   (if List.is_empty bd then mt () else str ":= ") ++
+                   prlist_with_sep (fun () -> str " <+")
+                   (pr_module_ast_inl true pr_lconstr) bd)
+        )
+      | VernacDeclareModule (export,id,bl,m1) ->
+        let b = pr_module_binders bl pr_lconstr in
+        return (
+          hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
+                   pr_lident id ++ b ++ str " :" ++
+                   pr_module_ast_inl true pr_lconstr m1)
+        )
+      | VernacDeclareModuleType (id,bl,tyl,m) ->
+        let b = pr_module_binders bl pr_lconstr in
+        let pr_mt = pr_module_ast_inl true pr_lconstr in
+        return (
+          hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
+                   prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
+                   (if List.is_empty m then mt () else str ":= ") ++
+                   prlist_with_sep (fun () -> str " <+ ") pr_mt m)
+        )
+      | VernacInclude (mexprs) ->
+        let pr_m = pr_module_ast_inl false pr_lconstr in
+        return (
+          hov 2 (keyword "Include" ++ spc() ++
+                   prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
+        )
+      (* Solving *)
+      | VernacSolveExistential (i,c) ->
+        return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
+
+      (* Auxiliary file and library management *)
+      | VernacAddLoadPath (fl,s,d) ->
+        return (
+          hov 2
+            (keyword "Add" ++
+               (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+               keyword "LoadPath" ++ spc() ++ qs s ++
+               (match d with
+                 | None -> mt()
+                 | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
+        )
+      | VernacRemoveLoadPath s ->
+        return (keyword "Remove LoadPath" ++ qs s)
+      | VernacAddMLPath (fl,s) ->
+        return (
+          keyword "Add"
+          ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
+          ++ keyword "ML Path"
+          ++ qs s
+        )
+      | VernacDeclareMLModule (l) ->
+        return (
+          hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+        )
+      | VernacChdir s ->
+        return (keyword "Cd" ++ pr_opt qs s)
+
+      (* Commands *)
+      | VernacCreateHintDb (dbname,b) ->
+        return (
+          hov 1 (keyword "Create HintDb" ++ spc () ++
+                   str dbname ++ (if b then str" discriminated" else mt ()))
+        )
+      | VernacRemoveHints (dbnames, ids) ->
+        return (
+          hov 1 (keyword "Remove Hints" ++ spc () ++
+                   prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
+                   pr_opt_hintbases dbnames)
+        )
+      | VernacHints (dbnames,h) ->
+        return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
+      | VernacSyntacticDefinition (id,(ids,c),compat) ->
+        return (
+          hov 2
+            (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
+               prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
+               pr_syntax_modifiers
+               (match compat with
+                | None -> []
+                | Some Flags.Current -> [SetOnlyParsing]
+                | Some v -> [SetCompatVersion v]))
+        )
+      | VernacArguments (q, args, more_implicits, nargs, mods) ->
+        return (
+          hov 2 (
+            keyword "Arguments" ++ spc() ++
+              pr_smart_global q ++
+              let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
+              let pr_if b x = if b then x else str "" in
+              let pr_br imp x = match imp with
+                | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
+                | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
+                | Vernacexpr.NotImplicit -> x in
+              let rec print_arguments n l =
+                match n, l with
+                  | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
+                  | _, [] -> mt()
+                  | n, { name = id; recarg_like = k;
+                         notation_scope = s;
+                         implicit_status = imp } :: tl ->
+                    spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
+                      print_arguments (Option.map pred n) tl
+              in
+              let rec print_implicits = function
+                | [] -> mt ()
+                | (name, impl) :: rest ->
+                   spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
+              in
+              print_arguments nargs args ++
+                if not (List.is_empty more_implicits) then
+                  prlist (fun l -> str"," ++ print_implicits l) more_implicits
+                else (mt ()) ++
+                (if not (List.is_empty mods) then str" : " else str"") ++
+                  prlist_with_sep (fun () -> str", " ++ spc()) (function
+                    | `ReductionDontExposeCase -> keyword "simpl nomatch"
+                    | `ReductionNeverUnfold -> keyword "simpl never"
+                    | `DefaultImplicits -> keyword "default implicits"
+                    | `Rename -> keyword "rename"
+                    | `Assert -> keyword "assert"
+                    | `ExtraScopes -> keyword "extra scopes"
+                    | `ClearImplicits -> keyword "clear implicits"
+                    | `ClearScopes -> keyword "clear scopes")
+                  mods)
+        )
+      | VernacReserve bl ->
+        let n = List.length (List.flatten (List.map fst bl)) in
+        return (
+          hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
+                 ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
+        )
+      | VernacGeneralizable g ->
+        return (
+          hov 1 (tag_keyword (
+            str"Generalizable Variable" ++
+              match g with
+                | None -> str "s none"
+                | Some [] -> str "s all"
+                | Some idl ->
+                  str (if List.length idl > 1 then "s " else " ") ++
+                    prlist_with_sep spc pr_lident idl)
+          ))
+      | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
+        return (
+          hov 1 (keyword "Transparent" ++
+                   spc() ++ prlist_with_sep sep pr_smart_global l)
+        )
+      | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+        return (
+          hov 1 (keyword "Opaque" ++
+                   spc() ++ prlist_with_sep sep pr_smart_global l)
+        )
+      | VernacSetOpacity _ ->
+        return (
+          CErrors.anomaly (keyword "VernacSetOpacity used to set something else.")
+        )
+      | VernacSetStrategy l ->
+        let pr_lev = function
+          | Conv_oracle.Opaque -> keyword "opaque"
+          | Conv_oracle.Expand -> keyword "expand"
+          | l when Conv_oracle.is_transparent l -> keyword "transparent"
+          | Conv_oracle.Level n -> int n
+        in
+        let pr_line (l,q) =
+          hov 2 (pr_lev l ++ spc() ++
+                   str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]")
+        in
+        return (
+          hov 1 (keyword "Strategy" ++ spc() ++
+                   hv 0 (prlist_with_sep sep pr_line l))
+        )
+      | VernacUnsetOption (export, na) ->
+        let export = if export then keyword "Export" ++ spc () else mt () in
+        return (
+          hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None)
+        )
+      | VernacSetOption (export, na,v) ->
+        let export = if export then keyword "Export" ++ spc () else mt () in
+        return (
+          hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v)
+        )
+      | VernacAddOption (na,l) ->
+        return (
+          hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
+        )
+      | VernacRemoveOption (na,l) ->
+        return (
+          hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l))
+        )
+      | VernacMemOption (na,l) ->
+        return (
+          hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l))
+        )
+      | VernacPrintOption na ->
+        return (
+          hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None)
+        )
+      | VernacCheckMayEval (r,io,c) ->
+        let pr_mayeval r c = match r with
+          | Some r0 ->
+            hov 2 (keyword "Eval" ++ spc() ++
+                     pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
+                     spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
+          | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
+        in
+        let pr_i = match io with None -> mt ()
+                               | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
+        return (pr_i ++ pr_mayeval r c)
+      | VernacGlobalCheck c ->
+        return (hov 2 (keyword "Type" ++ pr_constrarg c))
+      | VernacDeclareReduction (s,r) ->
+        return (
+          keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
+            pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
+        )
+      | VernacPrint p ->
+        return (pr_printable p)
+      | VernacSearch (sea,g,sea_r) ->
+        return (pr_search sea g sea_r pr_constr_pattern_expr)
+      | VernacLocate loc ->
+        let pr_locate =function
+          | LocateAny qid -> pr_smart_global qid
+          | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid
+          | LocateFile f -> keyword "File" ++ spc() ++ qs f
+          | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
+          | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
+          | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
+        in
+        return (keyword "Locate" ++ spc() ++ pr_locate loc)
+      | VernacRegister (id, RegisterInline) ->
+        return (
+          hov 2
+            (keyword "Register Inline" ++ spc() ++ pr_lident id)
+        )
+      | VernacComments l ->
+        return (
+          hov 2
+            (keyword "Comments" ++ spc()
+             ++ prlist_with_sep sep (pr_comment pr_constr) l)
+        )
+
+      (* For extension *)
+      | VernacExtend (s,c) ->
+        return (pr_extend s c)
+      | VernacProof (None, None) ->
+        return (keyword "Proof")
+      | VernacProof (None, Some e) ->
+        return (keyword "Proof " ++ spc () ++
+            keyword "using" ++ spc() ++ pr_using e)
+      | VernacProof (Some te, None) ->
+        return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te)
+      | VernacProof (Some te, Some e) ->
+        return (
+          keyword "Proof" ++ spc () ++
+            keyword "using" ++ spc() ++ pr_using e ++ spc() ++
+            keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te
+        )
+      | VernacProofMode s ->
+        return (keyword "Proof Mode" ++ str s)
+      | VernacBullet b ->
+        (* XXX: Redundant with Proof_bullet.print *)
+        return (let open Proof_bullet in begin match b with
+          | Dash n -> str (String.make n '-')
+          | Star n -> str (String.make n '*')
+          | Plus n -> str (String.make n '+')
+        end)
+      | VernacSubproof None ->
+        return (str "{")
+      | VernacSubproof (Some i) ->
+        return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
+      | VernacEndSubproof ->
+        return (str "}")
+
+let pr_vernac_flag =
+  function
+  | VernacPolymorphic true -> keyword "Polymorphic"
+  | VernacPolymorphic false -> keyword "Monomorphic"
+  | VernacProgram -> keyword "Program"
+  | VernacLocal local -> pr_locality local
+
+  let rec pr_vernac_control v =
+    let return = tag_vernac v in
+    match v with
+    | VernacExpr (f, v') ->
+      List.fold_right
+        (fun f a -> pr_vernac_flag f ++ spc() ++ a)
+        f
+        (pr_vernac_expr v' ++ sep_end v')
+    | VernacTime (_,{v}) ->
+      return (keyword "Time" ++ spc() ++ pr_vernac_control v)
+    | VernacRedirect (s, {v}) ->
+      return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
+    | VernacTimeout(n,v) ->
+      return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
+    | VernacFail v ->
+      return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
+
+    let pr_vernac v =
+      try pr_vernac_control v
+      with e -> CErrors.print e
diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli
new file mode 100644
index 000000000..4aa24bf5d
--- /dev/null
+++ b/vernac/ppvernac.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** This module implements pretty-printers for vernac_expr syntactic
+    objects and their subcomponents. *)
+
+val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
+
+(** Prints a fixpoint body *)
+val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
+
+(** Prints a vernac expression without dot *)
+val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t
+
+(** Prints a "proof using X" clause. *)
+val pr_using : Vernacexpr.section_subset_expr -> Pp.t
+
+(** Prints a vernac expression and closes it with a dot. *)
+val pr_vernac : Vernacexpr.vernac_control -> Pp.t
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
new file mode 100644
index 000000000..bac882381
--- /dev/null
+++ b/vernac/pvernac.ml
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*         *   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 Pcoq
+
+let uncurry f (x,y) = f x y
+
+let uvernac = create_universe "vernac"
+
+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 = new_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, [None, None, 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 () =
+  register_grammar Stdarg.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
new file mode 100644
index 000000000..9d999793e
--- /dev/null
+++ b/vernac/pvernac.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*         *   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 Pcoq
+open Genredexpr
+open Vernacexpr
+
+val uvernac : gram_universe
+
+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
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f001b572a..39c313ac7 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,10 +1,18 @@
+Vernacexpr
+Pvernac
+G_vernac
+G_proofs
 Vernacprop
-Proof_using
-Lemmas
 Himsg
 ExplainErr
-Class
 Locality
+Egramml
+Vernacinterp
+Ppvernac
+Proof_using
+Lemmas
+Class
+Egramcoq
 Metasyntax
 Auto_ind_decl
 Search
@@ -20,7 +28,6 @@ Classes
 Record
 Assumptions
 Vernacstate
-Vernacinterp
 Mltop
 Topfmt
 Vernacentries
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 65490bbbc..9a7f59085 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -977,7 +977,7 @@ let vernac_remove_hints ~atts dbs ids =
 
 let vernac_hints ~atts lb h =
   let local = enforce_module_locality atts.locality in
-  Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h)
+  Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h)
 
 let vernac_syntactic_definition ~atts lid x y =
   Dumpglob.dump_definition lid false "syndef";
@@ -1971,7 +1971,7 @@ let vernac_load interp fname =
     interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Gram.entry_parse Pcoq.main_entry po with
+    match Pcoq.Gram.entry_parse Pvernac.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
new file mode 100644
index 000000000..cf0da4de2
--- /dev/null
+++ b/vernac/vernacexpr.ml
@@ -0,0 +1,533 @@
+(************************************************************************)
+(*         *   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 = Hints.reference_or_constr =
+  | HintsReference of reference
+  | HintsConstr of constr_expr
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
+
+type hint_mode = Hints.hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
+
+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 = Hints.hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * Hints.reference_or_constr) list
+  | HintsImmediate of Hints.reference_or_constr list
+  | HintsUnfold of reference list
+  | HintsTransparency of reference list * bool
+  | HintsMode of reference * Hints.hint_mode list
+  | HintsConstructors of reference list
+  | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
+
+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.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"]