[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, 5 insertions, 3 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0ecfbacb09..b07a92658b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -416,8 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
       ComDefinition.do_definition
         ~program_mode:false
-        fname
-        Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl
+        ~name:fname
+        ~poly:false
+        ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+        ~kind:Decl_kinds.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
@@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
+       ComFixpoint.do_fixpoint ~scope:(Global ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->