- cic almost not used

[helm.git] / matita / components / ng_disambiguation / disambiguateChoices.mli

diff --git a/matita/components/ng_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli
index 4d1ed53296ba70c7608d396ed93303a5eebe5ddd..f96d90459f58aa6dfcd84bfe7c0b220d6d6d88b1 100644 (file)
--- a/matita/components/ng_disambiguation/disambiguateChoices.mli
+++ b/matita/components/ng_disambiguation/disambiguateChoices.mli
@@ -57,15 +57,12 @@ val lookup_symbol_by_dsc:
   term_of_nref: (NReference.reference -> 'term) ->
   string -> string -> 'term codomain_item
 
-val cic_lookup_symbol_by_dsc: 
-  string -> string -> Cic.term codomain_item
-
 val mk_choice:
   mk_appl: ('term list -> 'term) ->
   mk_implicit: (bool -> 'term) ->
   term_of_uri: (UriManager.uri -> 'term) ->
   term_of_nref: (NReference.reference -> 'term) ->
-  string * CicNotationPt.argument_pattern list *
-  CicNotationPt.cic_appl_pattern ->
+  string * NotationPt.argument_pattern list *
+  NotationPt.cic_appl_pattern ->
     'term codomain_item