Merge PR coq#19084: A few renamings or documentation of code here and…

… there to ease code understanding Reviewed-by: SkySkimmer Ack-by: ejgallego Co-authored-by: SkySkimmer <[email protected]>
SkySkimmer · May 30, 2024 · c67f36d · c67f36d
2 parents ac1e5eb + dc97559
commit c67f36d
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
@@ -470,7 +470,7 @@ let find_this_eq_data_decompose env sigma eqn =
 
 (*** Sigma-types *)
 
-let match_sigma env sigma ex =
+let match_sigma_data env sigma ex =
   match EConstr.kind sigma ex with
   | App (f, [| a; p; car; cdr |]) when is_lib_ref env sigma "core.sig.intro" f ->
       build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
@@ -479,7 +479,7 @@ let match_sigma env sigma ex =
   | _ -> raise PatternMatchingFailure
 
 let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *)
-  match_sigma env ex
+  match_sigma_data env ex
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern =

diff --git a/vernac/declare.ml b/vernac/declare.ml
@@ -2261,7 +2261,7 @@ let check_single_entry { entries; uctx } label =
   | _ ->
     CErrors.anomaly ~label Pp.(str "close_proof returned more than one proof term")
 
-let finalize_proof ~pm proof_obj proof_info =
+let finish_proof ~pm proof_obj proof_info =
   let open Proof_ending in
   match CEphemeron.default proof_info.Proof_info.proof_ending Regular with
   | Regular ->
@@ -2297,7 +2297,7 @@ let save ~pm ~proof ~opaque ~idopt =
   (* Env and sigma are just used for error printing in save_remaining_recthms *)
   let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in
   let proof_info = process_idopt_for_save ~idopt proof.pinfo in
-  finalize_proof ~pm proof_obj proof_info
+  finish_proof ~pm proof_obj proof_info
 
 let save_regular ~(proof : t) ~opaque ~idopt =
   let open Proof_ending in
@@ -2325,7 +2325,7 @@ let save_lemma_admitted_delayed ~pm ~proof =
 let save_lemma_proved_delayed ~pm ~proof ~idopt =
   (* vio2vo used to call this with invalid [pinfo], now it should work fine. *)
   let pinfo = process_idopt_for_save ~idopt proof.pinfo in
-  let pm, _ = finalize_proof ~pm proof pinfo in
+  let pm, _ = finish_proof ~pm proof pinfo in
   pm
 
 end (* Proof module *)

diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml
@@ -235,10 +235,10 @@ let retrieve_obligations env name evm fs ?deps ?status t ty =
   let evts =
     (* Remove existential variables in types and build the corresponding products *)
     List.fold_right
-      (fun (id, (n, nstr), ev) l ->
+      (fun (id, (n, nstr), ev) evs ->
         let hyps = Evd.evar_filtered_context ev in
         let hyps = trunc_named_context nc_len hyps in
-        let evtyp, deps, transp = etype_of_evar evm l hyps (Evd.evar_concl ev) in
+        let evtyp, deps, transp = etype_of_evar evm evs hyps (Evd.evar_concl ev) in
         let evtyp, hyps, chop =
           match chop_product fs evtyp with
           | Some t -> (t, trunc_named_context fs hyps, fs)
@@ -271,7 +271,7 @@ let retrieve_obligations env name evm fs ?deps ?status t ty =
           ; ev_deps = deps
           ; ev_tac = None }
         in
-        (id, info) :: l)
+        (id, info) :: evs)
       evn []
   in
   let t', _, transparent =