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

1 files changed, 9 insertions, 9 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ed207b52dd..b64af52b6e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -378,11 +378,11 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
-  let pstate = Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
+  let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
       ~hook:(Lemmas.mk_hook
                (fun _ _ _ -> instance_hook pri global imps ?hook)) in
   (* spiwack: I don't know what to do with the status here. *)
-  let pstate =
+  let lemma =
     if not (Option.is_empty term) then
       let init_refine =
         Tacticals.New.tclTHENLIST [
@@ -391,18 +391,18 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
           Tactics.New.reduce_after_refine;
         ]
       in
-      let pstate, _ = Pfedit.by init_refine pstate in
-      pstate
+      let lemma, _ = Lemmas.by init_refine lemma in
+      lemma
     else
-      let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
-      pstate
+      let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in
+      lemma
   in
   match tac with
   | Some tac ->
-    let pstate, _ = Pfedit.by tac pstate in
-    pstate
+    let lemma, _ = Lemmas.by tac lemma in
+    lemma
   | None ->
-    pstate
+    lemma
 
 let do_instance_subst_constructor_and_ty subst k u ctx =
   let subst =