[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.

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