X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=188726d9510879720ff984782cd5d8e26fe558d6;hb=b5619c04607ec92594e7645847409c351129709b;hp=4b1b994d97f8e01b22278d1a787fd084da688be1;hpb=efec9dde0ebb9ea6b8d8556b92bc0173dcab2cb7;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4b1b994d9..188726d95 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -509,7 +509,9 @@ object (self)
       bottom) and we will face a macro *)
    match self#grafite_status.proof_status with
       Incomplete_proof p ->
-       userGoal <- Some (Continuationals.Stack.find_goal p.stack)
+       userGoal <-
+         (try Some (Continuationals.Stack.find_goal p.stack)
+         with Failure _ -> None)
     | _ -> userGoal <- None
 
   method private _retract offset lexicon_status grafite_status new_statements