[proof] More uniformity in proof start labels.

4 files changed, 12 insertions, 12 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 64d21be7e8..98002de119 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -119,7 +119,7 @@ let next = let n = ref 0 in fun () -> incr n; !n
 let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) typ tac =
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof evd id ~poly UState.default_univ_decl goal_kind goals in
+  let pf = Proof_global.start_proof ~name:id ~poly ~udecl:UState.default_univ_decl ~kind:goal_kind evd goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 22f818edbb..8ac4435539 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -94,7 +94,7 @@ let set_endline_tactic tac ps =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma name udecl ~poly kind goals =
+let start_proof ~name ~udecl ~poly ~kind sigma goals =
   { proof = Proof.start ~name ~poly sigma goals
   ; endline_tactic = None
   ; section_vars = None
@@ -102,7 +102,7 @@ let start_proof sigma name udecl ~poly kind goals =
   ; strength = kind
   }
 
-let start_dependent_proof name udecl ~poly kind goals =
+let start_dependent_proof ~name ~udecl ~poly ~kind goals =
   { proof = Proof.dependent_start ~name ~poly goals
   ; endline_tactic = None
   ; section_vars = None
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 5bfed948ba..2c328bcf12 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -63,21 +63,21 @@ type opacity_flag = Opaque | Transparent
    typically contain universe constraints), and with universe bindings
    pl. *)
 val start_proof
-  :  Evd.evar_map
-  -> Names.Id.t
-  -> UState.universe_decl
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
   -> poly:bool
-  -> Decl_kinds.goal_kind
+  -> kind:Decl_kinds.goal_kind
+  -> Evd.evar_map
   -> (Environ.env * EConstr.types) list
   -> t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof
-  :  Names.Id.t
-  -> UState.universe_decl
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
   -> poly:bool
-  -> Decl_kinds.goal_kind
+  -> kind:Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d323493c11..744cdbfb5f 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -344,13 +344,13 @@ let start_lemma ~name ~poly ~kind
     ?(info=Info.make ())
     sigma c =
   let goals = [ Global.env_of_context sign , c ] in
-  let proof = Proof_global.start_proof sigma name udecl ~poly kind goals in
+  let proof = Proof_global.start_proof sigma ~name ~udecl ~poly ~kind goals in
   { proof ; info }
 
 let start_dependent_lemma ~name ~poly ~kind
     ?(udecl=UState.default_univ_decl)
     ?(info=Info.make ()) telescope =
-  let proof = Proof_global.start_dependent_proof name udecl ~poly kind telescope in
+  let proof = Proof_global.start_dependent_proof ~name ~udecl ~poly ~kind telescope in
   { proof; info }
 
 let rec_tac_initializer finite guard thms snl =