X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateChoices.mli;h=0ad498106456a50d50ed4962a530e597b7d1a08f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=87d731e274d33eb8889e215fb929f7da678b0398;hpb=45586ab88c026e6a21927654387b6df266a44700;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
index 87d731e27..0ad498106 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
@@ -27,44 +27,27 @@ open DisambiguateTypes
 
 (** {2 Choice registration low-level 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
-
   (** raised by lookup_XXXX below *)
-exception Choice_not_found of string
-
-  (** register a new symbol choice *)
-val add_symbol_choice: string -> codomain_item -> unit
+exception Choice_not_found of string Lazy.t
 
   (** register a new number choice *)
 val add_num_choice: codomain_item -> unit
 
-(** {2 Choice registration high-level interface} *)
-
-  (** @param symbol
-   * @param description
-   * @param term cic application head *)
-val add_binary_op: string -> string -> Cic.term -> unit
-
-  (** @param symbol
-   * @param description
-   * @param term cic application head *)
-val add_unary_op: string -> string -> Cic.term -> 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