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.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index a467c22ede..e82fb3e3b1 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,31 +36,31 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_definition ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
-  let gr = match local with
+  let gr = match scope with
   | Discharge ->
-      let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
-      VarRef ident
+      let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in
+      VarRef name
   | Global local ->
-      let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+      let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in
       let gr = ConstRef kn in
-      let () = Declare.declare_univ_binders gr pl in
+      let () = Declare.declare_univ_binders gr udecl in
       gr
   in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = definition_message ident in
+  let () = definition_message name in
   begin
     match hook_data with
     | None -> ()
     | Some (hook, uctx, extra_defs) ->
-      Hook.call ~fix_exn ~hook uctx extra_defs local gr
+      Hook.call ~fix_exn ~hook uctx extra_defs scope gr
   end;
   gr
 
-let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition f kind ?hook_data ce pl imps
+  declare_definition ~name ~scope ~kind ?hook_data udecl ce imps
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
-- 
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.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index e82fb3e3b1..d74fdcab2c 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -13,12 +13,14 @@ open Declare
 open Globnames
 open Impargs
 
+type locality = Discharge | Global of Declare.import_status
+
 (* Hooks naturally belong here as they apply to both definitions and lemmas *)
 module Hook = struct
   module S = struct
     type t = UState.t
       -> (Names.Id.t * Constr.t) list
-      -> Decl_kinds.locality
+      -> locality
       -> Names.GlobRef.t
       -> unit
   end
-- 
cgit v1.2.3