X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateChoices.mli;h=74dfaaa58bec3dc215ca1c38631a65bb4b406a5a;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=3a6e92f558de819af9b780967d10d4e2e5d3a96e;hpb=6459acbd4bb69475cfaa0b37a9771ced94193667;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
index 3a6e92f55..74dfaaa58 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
@@ -25,34 +25,29 @@
 
 open DisambiguateTypes
 
-(** {2 Choice registration interface} *)
-
-  (** to be raised when a choice is invalid due to some given parameter (e.g.
-   * wrong number of Cic.term arguments received) *)
-exception Invalid_choice
+(** {2 Choice registration low-level interface} *)
 
   (** raised by lookup_XXXX below *)
 exception Choice_not_found of string
 
-  (** register a new symbol choice *)
-val add_symbol_choice: string -> codomain_item -> unit
-
   (** register a new number choice *)
 val add_num_choice: codomain_item -> unit
 
 (** {2 Choices lookup}
  * for user defined aliases *)
 
-  (** @param symbol symbol as per AST *)
-val lookup_symbol_choices: string -> codomain_item list
-
 val lookup_num_choices: unit -> codomain_item list
 
+  (** @param dsc description (1st component of codomain_item) *)
+val lookup_num_by_dsc: string -> codomain_item
+
   (** @param symbol symbol as per AST
    * @param dsc description (1st component of codomain_item)
    *)
 val lookup_symbol_by_dsc: string -> string -> codomain_item
 
-  (** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> codomain_item
+val mk_choice:
+  string * CicNotationPt.argument_pattern list *
+  CicNotationPt.cic_appl_pattern ->
+    codomain_item