Initial implementation of statuses using objects in place of nested records.

[helm.git] / helm / software / components / grafite_engine / grafiteTypes.ml

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 0b9a4a7da8e161f75aa0d3ece109c6548f248fc7..6033be8c2c09cce599a63919822a32c75e930413 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -96,49 +96,11 @@ let set_estatus e x =
 
 let get_dstatus x = (get_estatus x).NEstatus.rstatus;;
 
-let get_rstatus x = (get_dstatus x).NRstatus.refiner_status;;
-
-let get_hstatus x = (get_rstatus x).NRstatus.uhint_db;;
-
-let get_library_db x = (get_rstatus x).NRstatus.library_db;;
-
-let get_dump x = (get_dstatus x).NRstatus.dump;;
-
 let set_dstatus h x =
  let estatus = get_estatus x in
   set_estatus { estatus with NEstatus.rstatus = h } x
 ;;
 
-let set_rstatus h x =
- let dstatus = get_dstatus x in
-  set_dstatus { dstatus with NRstatus.refiner_status = h } x
-;;
-
-let set_coercions db x = 
- let rstatus = get_rstatus x in
-  set_rstatus { rstatus with NRstatus.coerc_db = db } x
-;;
-
-
-let set_hstatus h x =
- let rstatus = get_rstatus x in
-  set_rstatus { rstatus with NRstatus.uhint_db = h} x
-;;
-
-let set_library_db h x =
- let rstatus = get_rstatus x in
-  set_rstatus { rstatus with NRstatus.library_db = h} x
-;;
-
-let set_dump h x =
- let estatus = get_estatus x in
-  set_estatus
-  { estatus with NEstatus.rstatus =
-     { estatus.NEstatus.rstatus with
-        NRstatus.dump = h}}
-  x
-;;
-
 let get_current_proof status =
   match status.proof_status with
   | Incomplete_proof { proof = p } -> p
@@ -271,5 +233,3 @@ let dump_status status =
   HLog.message "status.objects:\n";
   List.iter 
     (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects 
-  
-let get_coercions x = (get_rstatus x).NRstatus.coerc_db;;