]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/content/interpretations.mli
urimanager removed
[helm.git] / matita / components / content / interpretations.mli
index 10a2f093e1c6b90600f1e4d12d519345c922bd4f..50432801dd8acc107c025672fcc38baccc66bc44 100644 (file)
@@ -60,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