]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/content/interpretations.ml
fix queries
[helm.git] / matita / components / content / interpretations.ml
index c7bfa576804b19621429f46f9556a4158b1db350..8059eeaaecbac6f3b04497573ff788f1677c61a5 100644 (file)
@@ -28,7 +28,6 @@
 open Printf
 
 module Ast = NotationPt
-module Obj = LibraryObjects
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
@@ -37,9 +36,11 @@ type interpretation_id = int
 
 let idref id t = Ast.AttributedTerm (`IdRef id, t)
 
+type cic_id = string
+
 type term_info =
-  { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
-    uri: (Cic.id, UriManager.uri) Hashtbl.t;
+  { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
+    uri: (cic_id, UriManager.uri) Hashtbl.t;
   }
 
   (* persistent state *)