urimanager removed

[helm.git] / matita / components / content / interpretations.mli

diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli
index 222a340f4ea6de8f3c84c7ee0d18d200c2f56f96..50432801dd8acc107c025672fcc38baccc66bc44 100644 (file)
--- a/matita/components/content/interpretations.mli
+++ b/matita/components/content/interpretations.mli
@@ -28,6 +28,8 @@
 
 type interpretation_id
 
+type cic_id = string
+
 val add_interpretation:
   string ->                                       (* id / description *)
   string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
@@ -58,7 +60,6 @@ val set_active_interpretations: interpretation_id list -> unit
 val instantiate_appl_pattern:
   mk_appl:('term list -> 'term) -> 
   mk_implicit:(bool -> 'term) ->
-  term_of_uri : (UriManager.uri -> 'term) ->
   term_of_nref : (NReference.reference -> 'term) ->
   (string * 'term) list -> NotationPt.cic_appl_pattern ->
     'term