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

1 files changed, 10 insertions, 10 deletions

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