]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitaTypes.ml
universes in CicBrowser
[helm.git] / helm / software / matita / matitaTypes.ml
index 0c8952e89777016f954536df2f416895c5d0a6fc..18aaa2e6552a58c7cf4247d750cb143a6013505d 100644 (file)
@@ -48,6 +48,7 @@ type mathViewer_entry =
   | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
   | `Uri of UriManager.uri (* cic object uri *)
   | `Whelp of string * UriManager.uri list (* query and results *)
+  | `Univs of UriManager.uri
   ]
 
 let string_of_entry = function
@@ -72,6 +73,7 @@ let string_of_entry = function
           (match dir with | `Fwd -> "forward" | `Back -> "backward") ^ suri)
   | `Uri uri -> UriManager.string_of_uri uri
   | `Whelp (query, _) -> query
+  | `Univs uri -> "univs:" ^ UriManager.string_of_uri uri
 
 let entry_of_string = function
   | "about:blank" -> `About `Blank