diff options
| author | Emilio Jesus Gallego Arias | 2018-04-02 04:26:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-06 02:59:34 +0200 |
| commit | 79ff2bc044aa86a5ce30f0c24647db8c8e2544fa (patch) | |
| tree | ab262754c02841288ce18020bb03b28974f4858a /intf | |
| parent | b7938d0a51cdef8076bf5e1a58907b845a3fcc3d (diff) | |
[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.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 06f969f19c..4e1c986f16 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 |