X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotation.mli;h=1c6e95385a352f67072b094f4b5b677051d30bb5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=082f08b0589345b978681c9eab2c4d3554ed718b;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotation.mli b/helm/ocaml/cic_notation/cicNotation.mli
index 082f08b05..1c6e95385 100644
--- a/helm/ocaml/cic_notation/cicNotation.mli
+++ b/helm/ocaml/cic_notation/cicNotation.mli
@@ -33,3 +33,12 @@ val remove_notation: notation_id -> unit
 (** @param fname file from which load notation *)
 val load_notation: string -> unit
 
+(** {2 Notation enabling/disabling}
+ * Right now, only disabling of notation during pretty printing is supporting.
+ * If it is useful to disable it also for the input phase is still to be
+ * understood ... *)
+
+val get_all_notations: unit -> (notation_id * string) list  (* id, dsc *)
+val get_active_notations: unit -> notation_id list
+val set_active_notations: notation_id list -> unit
+