ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_notation / cicNotation.mli

diff --git a/helm/ocaml/cic_notation/cicNotation.mli b/helm/ocaml/cic_notation/cicNotation.mli
index 082f08b0589345b978681c9eab2c4d3554ed718b..1c6e95385a352f67072b094f4b5b677051d30bb5 100644 (file)
--- 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
+