Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.

Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: mattam82
Ack-by: maximedenes
Reviewed-by: ppedrot

3 files changed, 37 insertions, 26 deletions

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.");