[api] Remove dependency of library on Vernacexpr.

Morally, `library` should not depend on the vernacular
definition. This will also create problems when trying to modularize
the codebase due to the cycle [vernacs depend for example on
constrexprs].

The fix is fortunately easy.

10 files changed, 59 insertions, 16 deletions

diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh
new file mode 100644
index 000000000..7e554684e
--- /dev/null
+++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then
+
+    # Equations_CI_BRANCH=ssr+correct_packing
+    # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    # ltac2_CI_BRANCH=ssr+correct_packing
+    # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Elpi_CI_BRANCH=api+vernac_expr_iso
+    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+fi
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 06f969f19..4e1c986f1 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -281,20 +281,22 @@ type bullet =
 
 (** Rigid / flexible module signature *)
 
-type 'a 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 =
+type inline = Declaremods.inline =
   | NoInline
   | DefaultInline
   | InlineAt of int
+[@@ocaml.deprecated "please use [Declaremods.inline]."]
 
-type module_ast_inl = module_ast * 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
@@ -333,7 +335,7 @@ type nonrec vernac_expr =
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
-      inline * (ident_decl list * constr_expr) with_coercion list
+      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
@@ -373,7 +375,7 @@ type nonrec vernac_expr =
   | VernacDeclareModule of bool option * lident *
       module_binder list * module_ast_inl
   | VernacDefineModule of bool option * lident * module_binder list *
-      module_ast_inl module_signature * module_ast_inl 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
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 762efc5e3..1d5df49cf 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -17,11 +17,25 @@ open Entries
 open Libnames
 open Libobject
 open Mod_subst
-open Vernacexpr
 open Misctypes
 
 (** {6 Inlining levels} *)
 
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module inline annotations should we honor,
+    either None or the ones whose level is less or equal
+    to the given integer *)
+
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
+
 let default_inline () = Some (Flags.get_inline_level ())
 
 let inl2intopt = function
diff --git a/library/declaremods.mli b/library/declaremods.mli
index fd8d29614..4aee7feae 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -9,10 +9,24 @@
 (************************************************************************)
 
 open Names
-open Vernacexpr
 
 (** {6 Modules } *)
 
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module inline annotations should we honor,
+    either None or the ones whose level is less or equal
+    to the given integer *)
+
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
+
 type 'modast module_interpretor =
   Environ.env -> Misctypes.module_kind -> 'modast ->
     Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 593dcbf58..2dbd624c2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -17,6 +17,7 @@ open Constrexpr
 open Constrexpr_ops
 open Extend
 open Decl_kinds
+open Declaremods
 open Declarations
 open Misctypes
 open Tok (* necessary for camlp5 *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7eb8396ac..83c875707 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -16,12 +16,13 @@ open Util
 open CAst
 
 open Extend
-open Vernacexpr
-open Pputils
 open Libnames
+open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
-open Decl_kinds
+open Vernacexpr
+open Declaremods
+open Pputils
 
   open Ppconstr
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 76d427add..ae653974a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -425,7 +425,7 @@ let context poly l =
       let nstatus = match b with
       | None ->
         pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
-          Vernacexpr.NoInline (CAst.make id))
+               Declaremods.NoInline (CAst.make id))
       | Some b ->
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 6a590758f..26a46a752 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -20,7 +20,6 @@ open Constrintern
 open Impargs
 open Decl_kinds
 open Pretyping
-open Vernacexpr
 open Entries
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -66,7 +65,7 @@ match local with
 | Global | Local | Discharge ->
   let do_instance = should_axiom_into_instance local in
   let local = DeclareDef.get_locality ident ~kind:"axiom" local in
-  let inl = match nl with
+  let inl = let open Declaremods in match nl with
     | NoInline -> None
     | DefaultInline -> Some (Flags.get_inline_level())
     | InlineAt i -> Some i
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 56e324376..a2d20a1d1 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 (** {6 Parameters/Assumptions} *)
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
+  Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
 
 (************************************************************************)
 (** Internal API  *)
@@ -32,5 +32,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
 val declare_assumption : coercion_flag -> assumption_kind ->
   types in_constant_universes_entry ->
   Universes.universe_binders -> Impargs.manual_implicits ->
-  bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t ->
+  bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
   global_reference * Univ.Instance.t * bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b44c7cccb..11e9dc16c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -672,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
      else (idl,ty)) binders_ast in
   let mp =
     Declaremods.declare_module Modintern.interp_module_ast
-      id binders_ast (Enforce mty_ast) []
+      id binders_ast (Declaremods.Enforce mty_ast) []
   in
   Dumpglob.dump_moddef ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");