X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaTypes.ml;h=791713e56a4b5e13f2fa302cf7c87dac52796c6d;hb=f104e234238586ac846881feb30e1b56a509cfd3;hp=177cfb3af42ac179331ffc07ddb524c88d68b3fd;hpb=ae810c1e6bfab5076b18c841da9396a867526498;p=helm.git diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml index 177cfb3af..791713e56 100644 --- a/matita/matitaTypes.ml +++ b/matita/matitaTypes.ml @@ -40,9 +40,11 @@ type abouts = type mathViewer_entry = [ `About of abouts (* current proof *) - | `Check of string (* term *) + | `Check of string (* term *) | `Cic of Cic.term * Cic.metasenv - | `Dir of string (* "directory" in cic uris namespace *) + | `Development of string + | `Dir of string (* "directory" in cic uris namespace *) + | `HBugs of [ `Tutors ] (* list of available HBugs tutors *) | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri (* cic object uri *) | `Whelp of string * UriManager.uri list (* query and results *) @@ -55,7 +57,9 @@ let string_of_entry = function | `About `Coercions -> "about:coercions" | `Check _ -> "check:" | `Cic (_, _) -> "term:" + | `Development d -> "devel:/" ^ d | `Dir uri -> uri + | `HBugs `Tutors -> "hbugs:/tutors/" | `Metadata meta -> "metadata:/" ^ (match meta with