+ mk_appl:('term list -> 'term) ->
+ mk_implicit:(bool -> 'term) ->
+ term_of_uri : (UriManager.uri -> 'term) ->
+ term_of_nref : (NReference.reference -> 'term) ->
+ (string * 'term) list -> CicNotationPt.cic_appl_pattern ->
+ 'term
+
+val push: unit -> unit
+val pop: unit -> unit
+
+(* for Matita NG *)
+val find_level2_patterns32:
+ int ->
+ string * string *
+ CicNotationPt.argument_pattern list * CicNotationPt.cic_appl_pattern