diff options
| author | Emilio Jesus Gallego Arias | 2019-06-06 17:28:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:55:09 +0200 |
| commit | da5bbda84bd22b87a6057175c9d4d2391808e294 (patch) | |
| tree | c65591866875814ca83d99d28330d59dd4518452 /vernac | |
| parent | 9d65c49f05f946557df4c67b6e752f978e1e9352 (diff) | |
[api] [proof] Move `discharge` type to vernac_ast where it is used.
This seems like the right location, a bit more refactoring should be
possible.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/locality.ml | 3 | ||||
| -rw-r--r-- | vernac/locality.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 10 |
3 files changed, 8 insertions, 7 deletions
diff --git a/vernac/locality.ml b/vernac/locality.ml index 2f703b675e..f033d32874 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Decl_kinds - (** * Managing locality *) let importability_of_bool = function @@ -37,6 +35,7 @@ let warn_local_declaration = let enforce_locality_exp locality_flag discharge = let open DeclareDef in + let open Vernacexpr in match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) | None, NoDischarge -> Global Declare.ImportDefaultBehavior diff --git a/vernac/locality.mli b/vernac/locality.mli index 9c68b56a83..eda754324a 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -20,7 +20,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Decl_kinds.discharge -> DeclareDef.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> DeclareDef.locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 6a67a49d0a..dc5df5904e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -256,6 +256,8 @@ type extend_name = is given an offset, starting from zero. *) int +type discharge = DoDischarge | NoDischarge + type nonrec vernac_expr = | VernacLoad of verbose_flag * string @@ -274,15 +276,15 @@ type nonrec vernac_expr = | VernacDeclareCustomEntry of string (* Gallina *) - | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr + | VernacDefinition of (discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * + | VernacAssumption of (discharge * Decl_kinds.assumption_object_kind) * 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 + | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list |