X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FstatefulProofEngine.ml;h=9529c897c9362a214a7e88c559dc407b992b0667;hb=da59a744767c799ad287489c55f2ff972f93d93c;hp=13c1ac5144f66eee541a410072ccef2ccb223063;hpb=c71d85e81edbf2643df8267dbcf90d22031c9ea9;p=helm.git

diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml
index 13c1ac514..9529c897c 100644
--- a/helm/ocaml/tactics/statefulProofEngine.ml
+++ b/helm/ocaml/tactics/statefulProofEngine.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 let default_history_size = 20
 
 exception No_goal_left
@@ -94,6 +96,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 +107,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