From 78d6c353f0288a1b3b86aeb43b22a483c34822d9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Nov 2005 12:17:53 +0000 Subject: [PATCH] nicer (but convertible) types --- helm/matita/matitaTypes.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index 4fa2630de..ebf208b92 100644 --- 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 -- 2.39.2