big change in parsing, trying to make all functional

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

diff --git a/matita/components/lexicon/cicNotation.mli b/matita/components/lexicon/cicNotation.mli
index aa500f37115c6287d6269a85763172a9d2c6ca4f..16422729ba259a0340a43ab0286d7afad4003a91 100644 (file)
--- a/matita/components/lexicon/cicNotation.mli
+++ b/matita/components/lexicon/cicNotation.mli
@@ -23,27 +23,21 @@
  * http://helm.cs.unibo.it/
  *)
 
-type notation_id
-
 class type g_status =
  object ('self)
   inherit Interpretations.g_status
   inherit TermContentPres.g_status
+  inherit CicNotationParser.g_status
  end
 
 class status :
  object ('self)
   inherit Interpretations.status
   inherit TermContentPres.status
+  inherit CicNotationParser.status
   method set_notation_status: #g_status -> 'self
  end
 
-val compare_notation_id : notation_id -> notation_id -> int
-
 val process_notation:
- #status as 'status -> LexiconAst.command -> 'status * notation_id list
-
-val remove_notation: notation_id -> unit
+ #status as 'status -> LexiconAst.command -> 'status 
 
-val push: unit -> unit
-val pop: unit -> unit