From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 12 Oct 2004 20:56:45 +0000 (+0000)
Subject: setting goal doesn't change history status
X-Git-Tag: V_0_0_10~86
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59fb45409575e0f649604d276eaef04ce78b681e;p=helm.git

setting goal doesn't change history status
---

diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml
index 13c1ac514..f75442922 100644
--- a/helm/ocaml/tactics/statefulProofEngine.ml
+++ b/helm/ocaml/tactics/statefulProofEngine.ml
@@ -94,6 +94,8 @@ class ['a] status
       _data <- data
 
     method set_goal goal =
+      _goal <- Some goal
+(*
       let old_internal_status = self#internal_status in
       _goal <- Some goal;
       try
@@ -103,6 +105,7 @@ class ['a] status
       with (Data_failure _) as exn ->
         self#set_internal_status old_internal_status;
         raise exn
+*)
 
     method uri      = let (uri, _, _, _)      = _proof in uri
     method metasenv = let (_, metasenv, _, _) = _proof in metasenv