X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaProof.ml;h=ca1b4c9077f9bb32f5af79e0ddf4e5154e224e7e;hb=8fce28cde4e422993148e1fca011cae7ea230c16;hp=4f485445d45df0dba5918fab2301fa8bac88e3c8;hpb=1fa0472bfe2ed04c7adf166fa48df687f0022226;p=helm.git

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 4f485445d..ca1b4c907 100644
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -23,16 +23,16 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** create a Cic.CurrentProof from a given proof *)
-let currentProof (uri, metasenv, bo, ty) =
-  let uri = MatitaTypes.unopt_uri uri in
-    (* TODO CSC: Wrong: [] is just plainly wrong *)
-  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+open MatitaCicMisc
 
+let init_metadata _ = ()
+let compute_metadata _ _ = ()
+
+(*
 let init_metadata status =
   let ((_, metasenv, _, _) as proof, _) = status in
   let proof_object_metadata = (* compute proof annotations *)
-    Cic2acic.acic_object_of_cic_object (currentProof proof)
+    Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
   in
   let sequents_metadata = (* compute all sequent annotations from scratch *)
     List.map
@@ -43,9 +43,14 @@ let init_metadata status =
   (proof_object_metadata, sequents_metadata)
 
 let compute_metadata (old_status, old_metadata) new_status =
-  let ((_, new_metasenv, _, _) as new_proof, _) = new_status in
+  let ((_, new_metasenv, _, _) as new_proof, goal_opt) = new_status in
   let proof_object_metadata = (* compute proof annotations *)
-    Cic2acic.acic_object_of_cic_object (currentProof new_proof)
+    let obj =
+      match goal_opt with
+      | Some _ -> cicCurrentProof new_proof
+      | None -> cicConstant new_proof
+    in
+    Cic2acic.acic_object_of_cic_object obj
   in
   let sequents_metadata = (* compute all sequent annotations from scratch *)
     (** TODO Zack could we reuse some of the annotations from the previous
@@ -57,17 +62,18 @@ let compute_metadata (old_status, old_metadata) new_status =
       new_metasenv
   in
   (proof_object_metadata, sequents_metadata)
+*)
 
 class proof ?uri ~typ ~metasenv ~body () =
   object (self)
 
-    inherit [MatitaTypes.hist_metadata]
+    inherit [unit]
       StatefulProofEngine.status
-        ~history_size:BuildTimeConf.history_size ?uri ~typ ~body ~metasenv
+        ~history_size:BuildTimeConf.undo_history_size ?uri ~typ ~body ~metasenv
         init_metadata compute_metadata ()
 
     method toXml =
-      let currentproof = currentProof self#proof in
+      let currentproof = cicCurrentProof self#proof in
       let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
       in