[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.

6 files changed, 12 insertions, 13 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 2735a9118e..6eb582baef 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -10,8 +10,6 @@
 
 (** Informal mathematical status of declarations *)
 
-type discharge = DoDischarge | NoDischarge
-
 type binding_kind = Explicit | Implicit
 
 type private_flag = bool
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ef9d91c7fa..e20d010c71 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -182,7 +182,7 @@ let is_proof_termination_interactively_checked recsl =
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4e7f6a0ac6..aaba36287a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -87,7 +87,7 @@ let classify_vernac e =
         VtProofStep { parallel = `No;
                       proof_block_detection = Some "curly" }
     (* StartProof *)
-    | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
+    | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) ->
       VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
@@ -102,7 +102,7 @@ let classify_vernac e =
     | VernacFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -114,7 +114,7 @@ let classify_vernac e =
     | VernacCoFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
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