[tactics] Remove dependency of abstract on global proof state.

In order to do so we place the polymorphic status and name in the
read-only part of the monad.

Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.

Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.

Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.

25 files changed, 111 insertions, 141 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 77e34d4e00..f434b63d74 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -596,7 +596,7 @@ plugin:ci-elpi:
 plugin:ci-equations:
   <<: *ci-template
 
-plugin:ci-fiat-parsers:
+plugin:ci-fiat_parsers:
   <<: *ci-template
 
 plugin:ci-ltac2:
diff --git a/Makefile.ci b/Makefile.ci
index b8bff98f5f..0307d39d54 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -25,7 +25,7 @@ CI_TARGETS= \
     ci-fcsl-pcm \
     ci-fiat-crypto \
     ci-fiat-crypto-legacy \
-    ci-fiat-parsers \
+    ci-fiat_parsers \
     ci-flocq \
     ci-geocoq \
     ci-coqhammer \
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh
index ac74ebf667..ac74ebf667 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat_parsers.sh
diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
deleted file mode 100644
index 6e89741e29..0000000000
--- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then
-
-    bignums_CI_REF=primitive-integers
-    bignums_CI_GITURL=https://github.com/vbgl/bignums
-
-    mtac2_CI_REF=primitive-integers
-    mtac2_CI_GITURL=https://github.com/vbgl/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
deleted file mode 100644
index 2df8affd14..0000000000
--- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then
-
-    elpi_CI_REF=ltac+remove_aliases
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
deleted file mode 100644
index f2a113b118..0000000000
--- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then
-
-    mtac2_CI_REF=build+warn_50
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
deleted file mode 100644
index f532fdfc52..0000000000
--- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then
-
-    ltac2_CI_REF=proof_rework
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    mtac2_CI_REF=proof_rework
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
new file mode 100644
index 0000000000..23eb24c304
--- /dev/null
+++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then
+
+    ltac2_CI_REF=proofview+proof_info
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    fiat_parsers_CI_REF=proofview+proof_info
+    fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+fi
diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
deleted file mode 100644
index efcdd2e97f..0000000000
--- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then
-
-    paramcoq_CI_REF=stm-shallow-logic
-    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
deleted file mode 100644
index ebd1b524da..0000000000
--- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then
-
-    mtac2_CI_REF=proof-mode
-    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
-
-    ltac2_CI_REF=proof-mode
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    equations_CI_REF=proof-mode
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
deleted file mode 100644
index 985c2db74e..0000000000
--- a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then
-
-    math_classes_CI_REF=program-mode-flag
-    math_classes_CI_GITURL=https://github.com/maximedenes/math-classes
-
-    ltac2_CI_REF=program-mode-flag
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-
-    equations_CI_REF=thread-program
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/engine/proofview.ml b/engine/proofview.ml
index d4ad53ff5f..a725444e81 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -223,9 +223,9 @@ module Proof = Logical
 type +'a tactic = 'a Proof.t
 
 (** Applies a tactic to the current proofview. *)
-let apply env t sp =
+let apply ~name ~poly env t sp =
   let open Logic_monad in
-  let ans = Proof.repr (Proof.run t false (sp,env)) in
+  let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in
   let ans = Logic_monad.NonLogical.run ans in
   match ans with
   | Nil (e, info) -> iraise (TacticFailure e, info)
@@ -993,7 +993,10 @@ let tclTIME s t =
         tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
   in aux 0 t
 
-
+let tclProofInfo =
+  let open Proof in
+  Logical.current >>= fun P.{name; poly} ->
+  tclUNIT (name, poly)
 
 (** {7 Unsafe primitives} *)
 
@@ -1275,7 +1278,8 @@ module V82 = struct
   let of_tactic t gls =
     try
       let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
-      let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
+      let name, poly = Names.Id.of_string "legacy_pe", false in
+      let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
     with Logic_monad.TacticFailure e as src ->
       let (_, info) = CErrors.push src in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 286703c0dc..680a93f0cc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -156,10 +156,15 @@ type +'a tactic
     tactic has given up. In case of multiple success the first one is
     selected. If there is no success, fails with
     {!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
-                                                   * proofview
-                                                   * (bool*Evar.t list*Evar.t list)
-                                                   * Proofview_monad.Info.tree
+val apply
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Environ.env
+  -> 'a tactic
+  -> proofview
+  -> 'a * proofview
+       * (bool*Evar.t list*Evar.t list)
+       * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
 
@@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic
     identifying annotation if present *)
 val tclTIME : string option -> 'a tactic -> 'a tactic
 
+(** Internal, don't use. *)
+val tclProofInfo : (Names.Id.t * bool) tactic
+[@@ocaml.deprecated "internal, don't use"]
+
 (** {7 Unsafe primitives} *)
 
 (** The primitives in the [Unsafe] module should be avoided as much as
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 69341d97df..80eb9d0124 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -177,7 +177,7 @@ module P = struct
   type s = proofview * Environ.env
 
   (** Recording info trace (true) or not. *)
-  type e = bool
+  type e = { trace: bool; name : Names.Id.t; poly : bool }
 
   (** Status (safe/unsafe) * shelved goals * given up *)
   type w = bool * goal list
@@ -254,13 +254,16 @@ end
 
 (** Lens and utilies pertaining to the info trace *)
 module InfoL = struct
-  let recording = Logical.current
+  let recording = Logical.(map (fun {P.trace} -> trace) current)
   let if_recording t =
     let open Logical in
     recording >>= fun r ->
     if r then t else return ()
 
-  let record_trace t = Logical.local true t
+  let record_trace t =
+    Logical.(
+      current >>= fun s ->
+      local {s with P.trace = true} t)
 
   let raw_update = Logical.update
   let update f = if_recording (raw_update f)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index a08cab3bf6..3437b6ce77 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -98,7 +98,7 @@ module P : sig
   val wprod : w -> w -> w
 
   (** Recording info trace (true) or not. *)
-  type e = bool
+  type e = { trace: bool; name : Names.Id.t; poly : bool }
 
   type u = Info.state
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 525ff7fd0f..62906303a4 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -530,7 +530,15 @@ let interp_gen kind ist pattern_mode flags env sigma c =
       invariant that running the tactic returned by push_trace does
       not modify sigma. *)
   let (_, dummy_proofview) = Proofview.init sigma [] in
-  let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
+
+  (* Again this is called at times with no open proof! *)
+  let name, poly =
+    try
+      let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
+      name, poly
+    with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false
+  in
+  let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
   let (evd,c) =
     catch_error trace (understand_ltac flags env sigma vars kind) term
   in
@@ -2041,7 +2049,16 @@ let _ =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun = lfun; extra; } in
     let tac = interp_tactic ist tac in
-    let name, poly = Id.of_string "ltac_sub", false in
+    (* XXX: This depends on the global state which is bad; the hooking
+       mechanism should be modified. *)
+    let name, poly =
+      try
+        let (_, poly, _) = Proof_global.get_current_persistence () in
+        let name = Proof_global.get_current_proof_name () in
+        name, poly
+      with | Proof_global.NoCurrentProof ->
+        Id.of_string "ltac_gen", false
+    in
     let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7f1ae6d12b..9509c36ec0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -70,11 +70,6 @@ let get_current_context ?p () =
         let evd = Proof.in_proof p (fun x -> x) in
         (evd, Global.env ())
 
-let current_proof_statement () =
-  match Proof_global.V82.get_current_initial_conclusions () with
-    | (id,([concl],strength)) -> id,strength,concl
-    | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.")
-
 let solve ?with_end_tac gi info_lvl tac pr =
   try 
     let tac = match with_end_tac with
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5699320af5..29ab00876a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -34,11 +34,6 @@ val get_current_goal_context : unit -> Evd.evar_map * env
 
 val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env
 
-(** [current_proof_statement] *)
-
-val current_proof_statement :
-  unit -> Id.t * goal_kind * EConstr.types
-
 (** {6 ... } *)
 
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 4ce932b93d..e40940f652 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -415,8 +415,9 @@ let run_tactic env tac pr =
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT retrieved
   in
+  let { name; poly } = pr in
   let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
-    Proofview.apply env tac sp
+    Proofview.apply ~name ~poly env tac sp
   in
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
@@ -498,7 +499,8 @@ module V82 = struct
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
-    let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in
+    let { name; poly } = pr in
+    let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in
     let shelf =
       List.filter begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 9ee9e7ae2c..0cfc010c1a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -66,12 +66,6 @@ let pstates = ref ([] : pstate list)
 (* combinators for the current_proof lists *)
 let push a l = l := a::!l
 
-exception NoSuchProof
-let () = CErrors.register_handler begin function
-  | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
-  | _ -> raise CErrors.Unhandled
-end
-
 exception NoCurrentProof
 let () = CErrors.register_handler begin function
   | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
@@ -91,6 +85,7 @@ let cur_pstate () =
 let give_me_the_proof () = (cur_pstate ()).proof
 let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
 let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name
+let get_current_persistence () = (cur_pstate ()).strength
 
 let with_current_proof f =
   match !pstates with
@@ -386,15 +381,6 @@ let set_terminator hook =
   | [] -> raise NoCurrentProof
   | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
-module V82 = struct
-  let get_current_initial_conclusions () =
-  let { proof; strength } = cur_pstate () in
-  let Proof.{ name; entry } = Proof.data proof in
-  let initial = Proofview.initial_goals entry in
-  let goals = List.map (fun (o, c) -> c) initial in
-  name, (goals, strength)
-end
-
 let freeze ~marshallable =
   if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
   else !pstates
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 40920f51a3..38e234eaee 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -17,6 +17,7 @@ val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
 val get_current_proof_name : unit -> Names.Id.t
+val get_current_persistence : unit -> Decl_kinds.goal_kind
 val get_all_proof_names : unit -> Names.Id.t list
 
 val discard : Names.lident -> unit
@@ -104,8 +105,6 @@ val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t ->
 val get_terminator : unit -> proof_terminator
 val set_terminator : proof_terminator -> unit
 
-exception NoSuchProof
-
 val get_open_goals : unit -> int
 
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
@@ -129,11 +128,6 @@ val get_used_variables : unit -> Constr.named_context option
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : unit -> UState.universe_decl
 
-module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
-  Decl_kinds.goal_kind)
-end
-
 val freeze : marshallable:bool -> t
 val unfreeze : t -> unit
 val proof_of_state : t -> Proof.t
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 3a687a6b41..c3e3a62e26 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -11,7 +11,6 @@
 module CVars = Vars
 
 open Util
-open Names
 open Termops
 open EConstr
 open Decl_kinds
@@ -87,10 +86,26 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
+let name_op_to_name ~name_op ~name ~goal_kind suffix =
+  match name_op with
+  | Some s -> s, goal_kind
+  | None -> Nameops.add_suffix name suffix, goal_kind
+
+let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
+  Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (name, poly) ->
+  (* This is important: The [Global] and [Proof Theorem] parts of the
+     goal_kind are not relevant here as build_constant_by_tactic does
+     use the noop terminator; but beware if some day we remove the
+     redundancy on constrant declaration. This opens up an interesting
+     question, how does abstract behave when discharge is local for example?
+  *)
+  let goal_kind, suffix = if opaque
+    then (Global,poly,Proof Theorem), "_subproof"
+    else (Global,poly,DefinitionBody Definition), "_subterm" in
+  let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -126,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac
+    try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
@@ -170,26 +185,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac
   end
 
-let abstract_subproof ~opaque id gk tac =
-  cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> Tactics.exact_no_check (applist (lem, args)))
-
-let anon_id = Id.of_string "anonymous"
-
-let name_op_to_name name_op object_kind suffix =
-  let open Proof_global in
-  let default_gk = (Global, false, object_kind) in
-  let name, gk = match Proof_global.V82.get_current_initial_conclusions () with
-  | (id, (_, gk)) -> Some id, gk
-  | exception NoCurrentProof -> None, default_gk
-  in
-  match name_op with
-  | Some s -> s, gk
-  | None ->
-    let name = Option.default anon_id name in
-    Nameops.add_suffix name suffix, gk
+let abstract_subproof ~opaque tac =
+  cache_term_by_tactic_then ~opaque tac (fun lem args -> Tactics.exact_no_check (applist (lem, args)))
 
 let tclABSTRACT ?(opaque=true) name_op tac =
-  let s, gk = if opaque
-    then name_op_to_name name_op (Proof Theorem) "_subproof"
-    else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
-  abstract_subproof ~opaque s gk tac
+  abstract_subproof ~opaque ~name_op tac
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 7fb671fbf8..9d4f3cfb27 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -11,6 +11,12 @@
 open Names
 open EConstr
 
-val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+val cache_term_by_tactic_then
+  :  opaque:bool
+  -> name_op:Id.t option
+  -> ?goal_type:(constr option)
+  -> unit Proofview.tactic
+  -> (constr -> constr list -> unit Proofview.tactic)
+  -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ba7645446d..e505bb3a42 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -930,8 +930,16 @@ module Search = struct
        let _, pv = Proofview.init evm [] in
        let pv = Proofview.unshelve goals pv in
        try
+         (* Instance may try to call this before a proof is set up!
+            Thus, give_me_the_proof will fail. Beware! *)
+         let name, poly = try
+             let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
+             name, poly
+           with | Proof_global.NoCurrentProof ->
+             Id.of_string "instance", false
+         in
          let (), pv', (unsafe, shelved, gaveup), _ =
-           Proofview.apply env tac pv
+           Proofview.apply ~name ~poly env tac pv
          in
          if not (List.is_empty gaveup) then
            CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals.");
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4635883dc2..79182a3f9d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -481,7 +481,14 @@ let save_proof ?proof = function
             Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
         | None ->
             let pftree = Proof_global.give_me_the_proof () in
-            let id, k, typ = Pfedit.current_proof_statement () in
+            let gk = Proof_global.get_current_persistence () in
+            let Proof.{ name; poly; entry } = Proof.data pftree in
+            let typ = match Proofview.initial_goals entry with
+              | [typ] -> snd typ
+              | _ ->
+                CErrors.anomaly
+                  ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
+            in
             let typ = EConstr.Unsafe.to_constr typ in
             let universes = Proof.((data pftree).initial_euctx) in
             (* This will warn if the proof is complete *)
@@ -491,16 +498,15 @@ let save_proof ?proof = function
               if not !keep_admitted_vars then None
               else match Proof_global.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
-              | None, (pproof, _) :: _ -> 
+              | None, (pproof, _) :: _ ->
                   let env = Global.env () in
                   let ids_typ = Environ.global_vars_set env typ in
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
-            let poly = pi2 k in
             let ctx = UState.check_univ_decl ~poly universes decl in
-            Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
+            Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (opaque,idopt) ->