[declare] Bring more consistency to parameters using labels

Most of the parameters were named, we fix the remaining cases.

10 files changed, 46 insertions, 41 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 307214089f..2fdca15552 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,12 +1,12 @@
-let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps =
+let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
   let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
-      ~opaque ~poly sigma udecl ~types:tyopt ~body in
+      ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
-  let ubinders = Evd.universe_binders sigma in
+  let ubind = Evd.universe_binders sigma in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data
+  DeclareDef.declare_definition ~name ~scope ~kind ~ubind ce ~impargs ?hook_data
 
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
   edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-    ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl body None []
+    ~kind:Decls.(IsDefinition Definition) ~opaque:false ~impargs:[] ~udecl sigma body None
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 7bddbc994f..446026c4c8 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -295,8 +295,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       ~name:new_princ_name ~hook_data
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.(IsProof Theorem)
-      UnivNames.empty_binders
-      entry [] in
+      ~ubind:UnivNames.empty_binders
+      ~impargs:[]
+      entry in
   ()
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b1f7b2a0c3..29f5355fce 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -312,27 +312,27 @@ let instance_hook info global imps ?hook cst =
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant info global imps ?hook name decl poly sigma term termtype =
+let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
   let sigma, entry = DeclareDef.prepare_definition
-      ~allow_evars:false ~poly sigma decl ~types:(Some termtype) ~body:term in
+      ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
   let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
   Declare.definition_message name;
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
   instance_hook info global imps ?hook (GlobRef.ConstRef kn)
 
-let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name =
+let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
       [] subst (snd k.cl_context)
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
+  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook pri global imps (GlobRef.ConstRef cst)
+  instance_hook pri global impargs (GlobRef.ConstRef cst)
 
 let declare_instance_program env sigma ~global ~poly name pri imps univdecl term termtype =
   let hook { DeclareDef.Hook.S.scope; dref; _ } =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 8eff26bae5..dc9c8e2d3c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -204,7 +204,7 @@ let context_insection sigma ~poly ctx =
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
         let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry []
+            ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry
         in
         ()
     in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 8a0d0c9d81..26592b5542 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -70,7 +70,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
 
   let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode
-      ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in
+      ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in
 
   (ce, evd, udecl, imps)
 
@@ -80,7 +80,7 @@ let check_definition ~program_mode (ce, evd, _, imps) =
   ce
 
 let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt =
-  let (ce, evd, univdecl, imps as def) =
+  let (ce, evd, univdecl, impargs as def) =
     interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt
   in
   if program_mode then
@@ -99,10 +99,10 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
     in
     let ctx = Evd.evar_universe_context evd in
     ignore(Obligations.add_definition
-             ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls)
+             ~name ~term:c cty ctx ~univdecl ~implicits:impargs ~scope ~poly ~kind ?hook obls)
   else
     let ce = check_definition ~program_mode def in
     let uctx = Evd.evar_universe_context evd in
     let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
     let kind = Decls.IsDefinition kind in
-    ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps)
+    ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 8c050b800a..c266178594 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -294,11 +294,11 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
   let ctx = Evd.check_univ_decl ~poly evd pl in
-  let udecl = Evd.universe_binders evd in
+  let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    List.map4 (fun name body types imps ->
+    List.map4 (fun name body types impargs ->
         let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
-        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps)
+        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce)
       fixnames fixdecls fixtypes fiximps
   in
   recursive_message (not cofix) gidx fixnames;
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index a032ebf3f9..09582f4ef2 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -43,7 +43,7 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
+let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   let fix_exn = Declare.Internal.get_fix_exn ce in
   let should_suggest = ce.Declare.proof_entry_opaque &&
                        Option.is_empty ce.Declare.proof_entry_secctx in
@@ -56,10 +56,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
     let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
-    let () = DeclareUniv.declare_univ_binders gr udecl in
+    let () = DeclareUniv.declare_univ_binders gr ubind in
     gr
   in
-  let () = maybe_declare_manual_implicits false dref imps in
+  let () = maybe_declare_manual_implicits false dref impargs in
   let () = definition_message name in
   begin
     match hook_data with
@@ -95,7 +95,7 @@ let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
   if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
 
-let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body =
+let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma =
   check_definition_evars ~allow_evars sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
       sigma (fun nf -> nf body, Option.map nf types)
@@ -103,10 +103,10 @@ let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~bo
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, definition_entry ?opaque ?inline ?types ~univs body
 
-let prepare_parameter ~allow_evars ~poly sigma udecl typ =
+let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
   check_definition_evars ~allow_evars sigma;
   let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
-      sigma (fun nf -> nf typ)
+      sigma (fun nf -> nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, (None(*proof using*), (typ, univs), None(*inline*))
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1ff2145c0d..fb1fc9242c 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -44,9 +44,9 @@ val declare_definition
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> UnivNames.universe_binders
+  -> ubind:UnivNames.universe_binders
+  -> impargs:Impargs.manual_implicits
   -> Evd.side_effects Declare.proof_entry
-  -> Impargs.manual_implicits
   -> GlobRef.t
 
 val declare_assumption
@@ -64,12 +64,16 @@ val prepare_definition
   -> ?opaque:bool
   -> ?inline:bool
   -> poly:bool
-  -> Evd.evar_map
-  -> UState.universe_decl
+  -> udecl:UState.universe_decl
   -> types:EConstr.t option
   -> body:EConstr.t
+  -> Evd.evar_map
   -> Evd.evar_map * Evd.side_effects Declare.proof_entry
 
-val prepare_parameter : allow_evars:bool ->
-  poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
-  Evd.evar_map * Entries.parameter_entry
+val prepare_parameter
+  : allow_evars:bool
+  -> poly:bool
+  -> udecl:UState.universe_decl
+  -> types:EConstr.types
+  -> Evd.evar_map
+  -> Evd.evar_map * Entries.parameter_entry
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index a081aa3dae..a0be092e7e 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -348,12 +348,12 @@ let declare_definition prg =
   in
   let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
   let () = progmap_remove prg in
-  let ubinders = UState.universe_binders uctx in
+  let ubind = UState.universe_binders uctx in
   let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
   DeclareDef.declare_definition
-    ~name:prg.prg_name ~scope:prg.prg_scope ubinders
+    ~name:prg.prg_name ~scope:prg.prg_scope ~ubind
     ~kind:Decls.(IsDefinition prg.prg_kind) ce
-    prg.prg_implicits ?hook_data
+    ~impargs:prg.prg_implicits ?hook_data
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -429,12 +429,12 @@ let declare_mutual_definition l =
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
   let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
-  let udecl = UnivNames.empty_binders in
+  let ubind = UnivNames.empty_binders in
   let kns =
     List.map4
-      (fun name body types imps ->
+      (fun name body types impargs ->
          let ce = Declare.definition_entry ~opaque ~types ~univs body in
-         DeclareDef.declare_definition ~name ~scope ~kind udecl ce imps)
+         DeclareDef.declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c2cf7a5ec4..9b8bf6528b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -267,7 +267,7 @@ end = struct
     | Single pe ->
       (* We'd like to do [assert (i = 0)] here, however this codepath
          is used when declaring mutual cofixpoints *)
-      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs
+      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
     | Mutual pe ->
       (* if typ = None , we don't touch the type; used in the base case *)
       let pe =
@@ -278,7 +278,7 @@ end = struct
       in
       let pe = Declare.Internal.map_entry_body pe
           ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in
-      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs
+      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
 
   let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name { entry; info } =
     (* At some point make this a single iteration *)