Fixing abstract tactic by using a dummy name out of a declared proof.

1 files changed, 6 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e65e20c5f..969f9ef553 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3851,10 +3851,15 @@ let abstract_subproof id tac gl =
        success). Hence it reraises [e]. *)
     raise e
 
+let anon_id = Id.of_string "anonymous"
+
 let tclABSTRACT name_op tac gl =
+  let open Proof_global in
   let s = match name_op with
     | Some s -> s
-    | None   -> add_suffix (get_current_proof_name ()) "_subproof"
+    | None   ->
+      let name = try get_current_proof_name () with NoCurrentProof -> anon_id in
+      add_suffix name "_subproof"
   in
   abstract_subproof s tac gl