From 8b903319eae4d645f9385e8280d04d18a4f3a2bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 06:09:24 +0200
Subject: [lemmas] [proof] Split proof kinds into per-layer components.

We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:

- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
  pushed upwards]

We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.

More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
---
 vernac/declareDef.mli | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index ac4f44608b..708158814e 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -40,21 +40,23 @@ module Hook : sig
 end
 
 val declare_definition
-  : Id.t
-  -> definition_kind
+  :  name:Id.t
+  -> scope:locality
+  -> kind:definition_object_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> Evd.side_effects Proof_global.proof_entry
   -> UnivNames.universe_binders
+  -> Evd.side_effects Proof_global.proof_entry
   -> Impargs.manual_implicits
   -> GlobRef.t
 
 val declare_fix
-  : ?opaque:bool
+  :  ?opaque:bool
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> definition_kind
+  -> name:Id.t
+  -> scope:locality
+  -> kind:definition_object_kind
   -> UnivNames.universe_binders
   -> Entries.universes_entry
-  -> Id.t
   -> Evd.side_effects Entries.proof_output
   -> Constr.types
   -> Impargs.manual_implicits
-- 
cgit v1.2.3


From b2aae7ba35a90e695d34f904c74f5156385344a9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 13:21:48 +0200
Subject: [api] Move `locality` from `library` to `vernac`.

This datatype does belong to this layer.
---
 vernac/declareDef.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 708158814e..75fd5dcf5b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -11,6 +11,8 @@
 open Names
 open Decl_kinds
 
+type locality = Discharge | Global of Declare.import_status
+
 (** Declaration hooks *)
 module Hook : sig
   type t
@@ -28,7 +30,7 @@ module Hook : sig
       (** [(n1,t1),...(nm,tm)]: association list between obligation
           name and the corresponding defined term (might be a constant,
           but also an arbitrary term in the Expand case of obligations) *)
-      -> Decl_kinds.locality
+      -> locality
       (**  [locality]: Locality of the original declaration *)
       -> GlobRef.t
       (** [ref]: identifier of the origianl declaration *)
-- 
cgit v1.2.3


From 0c47ebf825690675cbb71153b8c9e4f7f6858984 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 11 Jun 2019 02:02:15 +0200
Subject: [proof] API Documentation fixes.

---
 vernac/declareDef.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 75fd5dcf5b..3934a29413 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -33,7 +33,7 @@ module Hook : sig
       -> locality
       (**  [locality]: Locality of the original declaration *)
       -> GlobRef.t
-      (** [ref]: identifier of the origianl declaration *)
+      (** [ref]: identifier of the original declaration *)
       -> unit
   end
 
-- 
cgit v1.2.3