[declare] Bring more consistency to parameters using labels

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

1 files changed, 4 insertions, 4 deletions

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)