X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.mli;h=bf6ee6a93498efd23714f61cdb00bd7b1a14479e;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=605a8f5ca36063be5b641eab2552289af0099053;hpb=6cc401c4136bafb6515bd39d86db6b5a917318bf;p=helm.git diff --git a/helm/software/components/acic_content/termAcicContent.mli b/helm/software/components/acic_content/termAcicContent.mli index 605a8f5ca..bf6ee6a93 100644 --- a/helm/software/components/acic_content/termAcicContent.mli +++ b/helm/software/components/acic_content/termAcicContent.mli @@ -68,8 +68,19 @@ val instantiate_appl_pattern: 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