X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.mli;h=1edacd96097139dcfee979838ef9781d949414a0;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=cd5f0876dd2fe4d715a5791c27f7f6ffeb7fb5ff;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationLexer.mli b/helm/software/components/content_pres/cicNotationLexer.mli
index cd5f0876d..1edacd960 100644
--- a/helm/software/components/content_pres/cicNotationLexer.mli
+++ b/helm/software/components/content_pres/cicNotationLexer.mli
@@ -32,9 +32,9 @@ exception Error of int * int * string
    * passing values of type char Stream.t, they should be in fact Ulexing.lexbuf
    * casted with Obj.magic :-/ Read the comment in the .ml for the rationale *)
 
-val level1_pattern_lexer: (string * string) Token.glexer
-val level2_ast_lexer: (string * string) Token.glexer
-val level2_meta_lexer: (string * string) Token.glexer
+val level1_pattern_lexer: unit -> (string * string) Token.glexer
+val level2_ast_lexer: unit -> (string * string) Token.glexer
+val level2_meta_lexer: unit -> (string * string) Token.glexer
 
   (** XXX ZACK DEFCON 4 END *)
 
@@ -43,6 +43,5 @@ val remove_level2_ast_keyword: string -> unit (** non idempotent *)
 
 (** {2 Ligatures} *)
 
-val is_ligature_char: char -> bool
-val lookup_ligatures: string -> string list
-
+val push: unit -> unit
+val pop: unit -> unit