X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.mli;h=acbe3bac6c4a606c8904a48e49b60a41d42acc56;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=4f2905a24873e42f62249047f83b9f7a47afd14a;hpb=3b5b254f2faa600a14a837e95f94f953dc9959c7;p=helm.git diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 4f2905a24..acbe3bac6 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -59,6 +59,8 @@ class type ['a] history = method previous : 'a (** @raise History_failure *) method load: 'a memento -> unit method save: 'a memento + method is_begin: bool + method is_end: bool end (** shell like history: new items added at the end of the history @@ -85,3 +87,6 @@ val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv val get_proof_context: MatitaTypes.status -> Cic.context val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment + (** given the base name of an image, returns its full path *) +val image_path: string -> string +