X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParserContext.mli;h=0b8871ee83aeb9a271ad280c45360380cb7d1fd9;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=7364eb6fc3f6ff6d272540adc80c6fc4b795c73c;hpb=818c90057de4f3ca2e1971b267549fe146b89b6f;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
index 7364eb6fc..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 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))