nicer (but convertible) types

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 4fa2630ded20825b6eadbdd1a521b8def073757b..ebf208b92954aa84a4243a61d32e3c785cfe2d79 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -70,9 +70,9 @@ val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
 val add_moo_metadata: GrafiteAst.metadata list -> status -> status
 
 val dump_status : status -> unit
-val get_option : status -> StringMap.key -> option_value
-val get_string_option : status -> StringMap.key -> string
-val set_option : status -> StringMap.key -> string -> status
+val get_option : status -> string -> option_value
+val get_string_option : status -> string -> string
+val set_option : status -> string -> string -> status
 
 class type console =
   object