From 79ff2bc044aa86a5ce30f0c24647db8c8e2544fa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 2 Apr 2018 04:26:09 +0200
Subject: [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.
---
 vernac/classes.ml        | 2 +-
 vernac/comAssumption.ml  | 3 +--
 vernac/comAssumption.mli | 4 ++--
 vernac/vernacentries.ml  | 2 +-
 4 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'vernac')

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");
-- 
cgit v1.2.3