* Undo fixed.

[helm.git] / helm / matita / matitaTypes.mli

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 321e26b99e9efcfdecae62346feb7fd3b3b1ad05..4fa2630ded20825b6eadbdd1a521b8def073757b 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -58,7 +58,7 @@ type status = {
   moo_content_rev: GrafiteMarshal.moo;
   proof_status: proof_status;                             (** logical status *)
   options: options;
-  objects: (UriManager.uri * string) list;  (** in-scope objects, with paths *)
+  objects: UriManager.uri list;  (** in-scope objects *)
   coercions: UriManager.uri list;                      (** defined coercions *)
   notation_ids: CicNotation.notation_id list;      (** in-scope notation ids *)
 }