X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParserContext.mli;h=23ad4af115ef8edd9205c1a2298d4db3dd81aec3;hb=71b08b1ea99893b3c5e2d91fc26e1ab7330fd33d;hp=837628b21c6848bfe481e36143b2f99019fd59c3;hpb=faf328f5779a7281c9c0588680b1b7bb89ae7640;p=helm.git diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli index 837628b21..23ad4af11 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli @@ -24,6 +24,10 @@ *) val main : - current_uri:(UriManager.uri) -> context:((Cic.name option) list) -> - metasenv:Cic.metasenv -> (Lexing.lexbuf -> CicTextualParser.token) -> - Lexing.lexbuf -> (Cic.metasenv * Cic.term) option + context:((Cic.name option) list) -> + metasenv:Cic.metasenv -> + (Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf -> + register_aliases:((string * CicTextualParser0.uri) -> unit) -> + (string list * + ((string -> CicTextualParser0.uri option) -> (Cic.metasenv * Cic.term)) + ) option