]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: when looking for a goal from the continuationals stack handle the case that...
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 20 Jan 2006 12:20:30 +0000 (12:20 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 20 Jan 2006 12:20:30 +0000 (12:20 +0000)
helm/matita/matitaScript.ml

index 4b1b994d97f8e01b22278d1a787fd084da688be1..188726d9510879720ff984782cd5d8e26fe558d6 100644 (file)
@@ -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