Merge PR #9566: [proof] Move proofs that have an associated constant to `Lemmas`

Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot

4 files changed, 11 insertions, 12 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0ded60d9c7..7691ca225e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -934,7 +934,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars STATE proof
 | [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.V82.grab_evars p) pstate }
+  -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -966,7 +966,7 @@ END
 VERNAC COMMAND EXTEND Unshelve STATE proof
 | [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.unshelve p) pstate  }
+  -> { fun ~pstate -> Proof_global.map_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 960e5b76f8..d10d10a664 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -376,7 +376,7 @@ let () = declare_int_option {
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Proof_global.with_proof (fun etac p ->
+  let pstate, status = Proof_global.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
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b99e77ab2b..2da6584aba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1962,7 +1962,6 @@ let add_setoid atts binders a aeq t n =
      (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
      (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
 
-
 let make_tactic name =
   let open Tacexpr in
   let tacqid = Libnames.qualid_of_string name in
@@ -1988,7 +1987,7 @@ let add_morphism_as_parameter atts m n : unit =
                   (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
   declare_projection n instance_id (ConstRef cst)
 
-let add_morphism_interactive atts m n : Proof_global.t =
+let add_morphism_interactive atts m n : Lemmas.t =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
@@ -2010,8 +2009,8 @@ let add_morphism_interactive atts m n : Proof_global.t =
   let hook = Lemmas.mk_hook hook in
   Flags.silently
     (fun () ->
-       let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
-       fst Pfedit.(by (Tacinterp.interp tac) pstate)) ()
+       let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
   init_setoid ();
@@ -2023,12 +2022,12 @@ let add_morphism atts binders m s n =
        [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let _id, pstate = Classes.new_instance_interactive
+  let _id, lemma = Classes.new_instance_interactive
       ~global:atts.global atts.polymorphic
       instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
-  pstate (* no instance body -> always open proof *)
+  lemma (* no instance body -> always open proof *)
 
 (** Bind to "rewrite" too *)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 3ef33c6dc9..a5c3782b30 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,16 +101,16 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t
 val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism
-  : rewrite_attributes
+  :  rewrite_attributes
   -> local_binder_expr list
   -> constr_expr
   -> constr_expr
   -> Id.t
-  -> Proof_global.t
+  -> Lemmas.t
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr