many changes regarding coercions:

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

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index ce988944bf7e2b574fd57bdf7cd8463ab5c575ba..95f65f3601c84d63ca53b533d57700a1da7623f7 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -42,20 +42,11 @@ type proof_status =
   | Proof of ProofEngineTypes.proof
   | Intermediate of Cic.metasenv
 
-(*
-type option_value =
-  | String of string
-  | Int of int
-type options
-val no_options: options
-*)
-
 type status = {
   moo_content_rev: GrafiteMarshal.moo;
   proof_status: proof_status;                             (** logical status *)
-(*   options: options; *)
   objects: UriManager.uri list;  (** in-scope objects *)
-  coercions: UriManager.uri list; (** defined coercions *)
+  coercions: CoercDb.coerc_db;
   universe:Universe.universe;  (** universe of terms used by auto *)
   baseuri: string;
 }