type pretty_printer_id
val add_pretty_printer:
- precedence:int ->
- associativity:Gramext.g_assoc ->
CicNotationPt.term -> (* level 2 pattern *)
- CicNotationPt.term -> (* level 1 pattern *)
+ CicNotationParser.checked_l1_pattern ->
pretty_printer_id
exception Pretty_printer_not_found
CicNotationEnv.t -> CicNotationPt.term ->
CicNotationPt.term
-(* hack. seee cicNotation for explanation *)
-val reset: unit -> unit
+val push: unit -> unit
+val pop: unit -> unit