Merge PR #11999: [proof] Merge `Proof_global` into `Declare`

Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: ppedrot

4 files changed, 8 insertions, 8 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7b1aa7a07a..7754fe401e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -346,7 +346,7 @@ open Vars
 
 let constr_flags () = {
   Pretyping.use_typeclasses = Pretyping.UseTC;
-  Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
+  Pretyping.solve_unification_constraints = Proof.use_unification_heuristics ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true;
   Pretyping.program_mode = false;
@@ -918,7 +918,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars STATE proof
 | [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+  -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
 VERNAC COMMAND EXTEND Unshelve STATE proof
 | [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.map_proof (fun p  -> Proof.unshelve p) pstate  }
+  -> { fun ~pstate -> Declare.Proof.map_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -1102,7 +1102,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Proof_global.compact_the_proof pstate }
+  { fun ~pstate -> Declare.Proof.compact pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 2bd4211c90..e713ab13b2 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -364,12 +364,12 @@ let print_info_trace =
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info (print_info_trace ()) in
       let (p,status) =
-        Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+        Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
       in
       (* in case a strict subtree was completed,
          go back to the top of the prooftree *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 321b05b97c..820063c25c 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -639,7 +639,7 @@ let solve_remaining_by env sigma holes by =
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
         let name, poly = Id.of_string "rewrite", false in
-        let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
+        let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in
         Evd.define evk (EConstr.of_constr c) sigma
     in
     List.fold_left solve sigma indep
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b0e26e1def..dda7f0742c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2070,7 +2070,7 @@ let _ =
      *)
     let name, poly = Id.of_string "ltac_gen", poly in
     let name, poly = Id.of_string "ltac_gen", poly in
-    let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
+    let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_tactic eval