From 79ff2bc044aa86a5ce30f0c24647db8c8e2544fa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias 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/comAssumption.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'vernac/comAssumption.ml') 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 -- cgit v1.2.3