X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateChoices.mli;h=87d731e274d33eb8889e215fb929f7da678b0398;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;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..87d731e27 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
@@ -25,7 +25,7 @@
 
 open DisambiguateTypes
 
-(** {2 Choice registration interface} *)
+(** {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) *)
@@ -40,6 +40,18 @@ val add_symbol_choice: string -> codomain_item -> unit
   (** 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 *)