snapshot

[helm.git] / helm / matita / matitaProof.ml

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 98b9cf02c85178f85c71e528759b891075caa07e..17b44ffd3ee600ca79af6e2d7d123c2fd01ef7b6 100644 (file)
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -23,26 +23,25 @@
  * 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, [])
+
 class proof ?uri ~typ ~metasenv ~body () =
   object (self)
 
-    inherit [unit] StatefulProofEngine.status ?uri ~typ ~body ~metasenv
-      (fun _ -> ())
-      (fun _ _ -> ())
-      ()
-
-    method private currentProof =
-      let (uri, metasenv, bo, ty) = self#proof in
-      let uri =
-        match uri with
-        | Some uri -> uri
-        | None -> MatitaTypes.untitled_con_uri
-      in
-        (* TODO CSC: Wrong: [] is just plainly wrong *)
-      Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+    inherit [MatitaTypes.hist_metadata]
+      StatefulProofEngine.status ?uri ~typ ~body ~metasenv
+        (fun proof ->
+          Cic2acic.acic_object_of_cic_object (currentProof (fst proof)))
+        (fun (old_proof, old_metadata) new_proof ->
+          Cic2acic.acic_object_of_cic_object (currentProof (fst new_proof)))
+        ()
 
     method toXml =
-      let currentproof = self#currentProof in
+      let currentproof = currentProof self#proof in
       let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
       in