]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_disambiguation/disambiguateChoices.mli
Cic.term and Cic.obj unused!
[helm.git] / matita / components / ng_disambiguation / disambiguateChoices.mli
index f96d90459f58aa6dfcd84bfe7c0b220d6d6d88b1..cdb7004a6abcd1f163989bbcff267f6795efa28e 100644 (file)
@@ -30,20 +30,12 @@ open DisambiguateTypes
   (** raised by lookup_XXXX below *)
 exception Choice_not_found of string Lazy.t
 
-  (** register a new number choice *)
-val add_num_choice: Cic.term codomain_item -> unit
-
   (** register a new number choice *)
 val nadd_num_choice: NCic.term codomain_item -> unit
 
 (** {2 Choices lookup}
  * for user defined aliases *)
 
-val lookup_num_choices: unit -> Cic.term codomain_item list
-
-  (** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> Cic.term codomain_item
-
   (** @param dsc description (1st component of codomain_item) *)
 val nlookup_num_by_dsc: string -> NCic.term codomain_item