X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParserContext.mli;h=0b8871ee83aeb9a271ad280c45360380cb7d1fd9;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=0ab69cdd55bbc85918e4ee90833fa1470ab0bc2e;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli index 0ab69cdd5..0b8871ee8 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli @@ -24,6 +24,8 @@ *) val main : - current_uri:(UriManager.uri) -> context:((Cic.name option) list) -> - (Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf -> - Cic.term option + context:((Cic.name option) list) -> + metasenv:Cic.metasenv -> + (Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf -> + CicTextualParser0.interpretation_domain_item list * + (CicTextualParser0.interpretation -> (Cic.metasenv * Cic.term))