From 069304b4e3ba75c54e372615bf7bb0ee2a103b5d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 2 Mar 2020 01:00:56 -0500
Subject: [declare] Bring more consistency to parameters using labels

Most of the parameters were named, we fix the remaining cases.
---
 vernac/declareDef.mli | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'vernac/declareDef.mli')

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
-- 
cgit v1.2.3