]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/ng_cic_content/interpretations.mli
Compilation fix
[helm.git] / matitaB / components / ng_cic_content / interpretations.mli
index b2c59b9c9b63e04ca2faa8af3dcb0e723525d250..4665be92c4a1d0e5f37cfe3bad36048e617dd28d 100644 (file)
@@ -92,6 +92,4 @@ val nmap_sequent:
    NotationPt.sequent 
 
 val nmap_obj:
- #status -> NCic.obj ->
-  NotationPt.term Content.cobj *
-   (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
+ #status -> NCic.obj -> NotationPt.term NotationPt.obj