bugfix: when looking for a goal from the continuationals stack handle the case that...

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4b1b994d97f8e01b22278d1a787fd084da688be1..188726d9510879720ff984782cd5d8e26fe558d6 100644 (file)
--- 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 ->
       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
     | _ -> userGoal <- None
 
   method private _retract offset lexicon_status grafite_status new_statements