added a lot of notation: arithmetic operators, relational operators, ...

[helm.git] / helm / ocaml / cic_disambiguation / disambiguateChoices.mli

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli
index 3a6e92f558de819af9b780967d10d4e2e5d3a96e..87d731e274d33eb8889e215fb929f7da678b0398 100644 (file)
--- 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 *)