From d400485650323689f9e09d202dfefe24e3ecfaac Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 27 Nov 2013 18:59:16 +0100
Subject: Fixing abstract tactic by using a dummy name out of a declared proof.

---
 tactics/tactics.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3