- 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)))
+ ()