* Undo fixed.

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 2d59ef95dea0c8d4df5b1aa469a9006ab8f98ead..dc692f8904cbd441273a27ec54f7d952f23b5189 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -71,7 +71,7 @@ type status = {
   moo_content_rev: moo;
   proof_status: proof_status;
   options: options;
-  objects: (UriManager.uri * string) list;
+  objects: UriManager.uri list;
   coercions: UriManager.uri list;
   notation_ids: CicNotation.notation_id list;
 }
@@ -108,8 +108,7 @@ let dump_status status =
   HLog.message "status.coercions\n";
   HLog.message "status.objects:\n";
   List.iter 
-    (fun (u,_) -> 
-      HLog.message (UriManager.string_of_uri u)) status.objects 
+    (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects 
   
 let get_option status name =
   try