Updated to use the new parser that creates (stacks of) existential variables

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParserContext.mli

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
index 0ab69cdd55bbc85918e4ee90833fa1470ab0bc2e..837628b21c6848bfe481e36143b2f99019fd59c3 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
@@ -25,5 +25,5 @@
 
 val main :
   current_uri:(UriManager.uri) -> context:((Cic.name option) list) ->
-   (Lexing.lexbuf  -> CicTextualParser.token) -> Lexing.lexbuf ->
-     Cic.term option
+   metasenv:Cic.metasenv -> (Lexing.lexbuf  -> CicTextualParser.token) ->
+   Lexing.lexbuf -> (Cic.metasenv * Cic.term) option