WARNING: partial commit (does not compile)

[helm.git] / matita / components / lexicon / cicNotation.mli

diff --git a/matita/components/lexicon/cicNotation.mli b/matita/components/lexicon/cicNotation.mli
index 9e231e3317a84f502e4e9558e57187dde8227536..085feda0dee3d435da4c49f8ec614755bad58498 100644 (file)
--- a/matita/components/lexicon/cicNotation.mli
+++ b/matita/components/lexicon/cicNotation.mli
@@ -27,18 +27,11 @@ type notation_id
 
 val compare_notation_id : notation_id -> notation_id -> int
 
-val process_notation: LexiconAst.command -> notation_id list
+val process_notation:
+ #Interpretations.status as 'status -> LexiconAst.command
+  -> 'status * notation_id list
 
 val remove_notation: notation_id -> unit
 
-(** {2 Notation enabling/disabling}
- * Right now, only disabling of notation during pretty printing is supported.
- * 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
-
 val push: unit -> unit
 val pop: unit -> unit