[api] Move `Vernacexpr` to parsing.

There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.

10 files changed, 15 insertions, 15 deletions

diff --git a/META.coq b/META.coq
index 3414ccbd4..12d7666cb 100644
--- a/META.coq
+++ b/META.coq
@@ -131,10 +131,10 @@ package "interp" (
 
 package "grammar" (
 
-  description = "Coq Base Grammar"
+  description = "Coq Camlp5 Grammar Extensions for Plugins"
   version     = "8.8"
 
-  requires    = "coq.interp"
+  requires    = "camlp5.gramlib"
   directory   = "grammar"
 
   archive(byte)   = "grammar.cma"
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bc6a1ef3a..74618a290 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
 let dump_definition {CAst.loc;v=id} sec s =
   dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
 
-let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
+let dump_constraint { CAst.loc; v = n } sec ty =
   match n with
     | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
     | Names.Anonymous -> ()
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 8dfb4f8f7..bf83d2df4 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -38,8 +38,8 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit
 val dump_notation :
   (Constrexpr.notation * Notation.notation_location) Loc.located ->
   Notation_term.scope_name option -> bool -> unit
-val dump_constraint :
-  Vernacexpr.typeclass_constraint -> bool -> string -> unit
+
+val dump_constraint : Misctypes.lname -> bool -> string -> unit
 
 val dump_string : string -> unit
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 58df9abc4..289890544 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -58,7 +58,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj =
     classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
   }
 
-let declare_generalizable local gen =
+let declare_generalizable ~local gen =
  Lib.add_anonymous_leaf (in_generalizable (local, gen))
 
 let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 5f4129ae0..39d0174f9 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -13,7 +13,7 @@ open Glob_term
 open Constrexpr
 open Libnames
 
-val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
 val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
diff --git a/pretyping/extend.ml b/parsing/extend.ml
index 734b859f6..734b859f6 100644
--- a/pretyping/extend.ml
+++ b/parsing/extend.ml
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 1f29636b2..103e1188a 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,5 +1,7 @@
 Tok
 CLexer
+Extend
+Vernacexpr
 Pcoq
 Egramml
 Egramcoq
diff --git a/pretyping/vernacexpr.ml b/parsing/vernacexpr.ml
index 71a2e8cb8..6ebf66349 100644
--- a/pretyping/vernacexpr.ml
+++ b/parsing/vernacexpr.ml
@@ -216,7 +216,7 @@ type syntax_modifier =
 type proof_end =
   | Admitted
   (*                         name in `Save ident` when closing goal *)
-  | Proved of opacity_flag * lident option
+  | Proved of Proof_global.opacity_flag * lident option
 
 type scheme =
   | InductionScheme of bool * reference or_by_notation * sort_expr
@@ -351,14 +351,14 @@ type nonrec vernac_expr =
   | VernacCoercion of reference or_by_notation *
       class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
-  | VernacNameSectionHypSet of lident * section_subset_expr 
+  | 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 *)
+        typeclass_constraint * (* instance name, class name, params *)
+        (bool * constr_expr) option * (* props *)
         Typeclasses.hint_info_expr
 
   | VernacContext of local_binder_expr list
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index d98026bc6..c48decdb0 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -27,8 +27,6 @@ Pattern
 Patternops
 Constr_matching
 Tacred
-Extend
-Vernacexpr
 Typeclasses_errors
 Typeclasses
 Classops
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 48deea97f..e1ce4e194 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -855,7 +855,7 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 let vernac_instance ~atts abst sup inst props pri =
   let global = not (make_section_locality atts.locality) in
-  Dumpglob.dump_constraint inst false "inst";
+  Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
   let program_mode = Flags.is_program_mode () in
   ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
 
@@ -1268,7 +1268,7 @@ let vernac_reserve bl =
 
 let vernac_generalizable ~atts =
   let local = make_non_locality atts.locality in
-  Implicit_quantifiers.declare_generalizable local
+  Implicit_quantifiers.declare_generalizable ~local
 
 let _ =
   declare_bool_option