- 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 4e9807932d41efa843b6e8450cdb92cc6145c7b8..f96d90459f58aa6dfcd84bfe7c0b220d6d6d88b1 100644 (file)
--- a/matita/components/ng_disambiguation/disambiguateChoices.mli
+++ b/matita/components/ng_disambiguation/disambiguateChoices.mli
@@ -57,9 +57,6 @@ 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) ->