X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateChoices.mli;h=0ad498106456a50d50ed4962a530e597b7d1a08f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;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..0ad498106 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
@@ -25,17 +25,10 @@
 
 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
+exception Choice_not_found of string Lazy.t
 
   (** register a new number choice *)
 val add_num_choice: codomain_item -> unit
@@ -43,16 +36,18 @@ 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