(** @raise Interpretation_not_found *)
val lookup_interpretations:
- string -> (* symbol *)
+ ?sorted:bool -> string -> (* symbol *)
(string * CicNotationPt.argument_pattern list *
CicNotationPt.cic_appl_pattern) list
(** {2 acic -> content} *)
val ast_of_acic:
+ output_type:[`Pattern|`Term] ->
(Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *)
Cic.annterm -> (* acic *)
CicNotationPt.term (* ast *)
(** @param env environment from argument_pattern to cic terms
* @param pat cic_appl_pattern *)
val instantiate_appl_pattern:
- (string * Cic.term) list -> CicNotationPt.cic_appl_pattern ->
- Cic.term
+ 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
+
+val add_load_patterns32:
+ ((bool * CicNotationPt.cic_appl_pattern * int) list -> unit) -> unit
+val init: unit -> unit