]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
lazily ==> call_by_name (since it is really a call_by_name!)
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParserContext.mli
index 837628b21c6848bfe481e36143b2f99019fd59c3..c83ac03f8b1df4beeb2cfccfa3dad241ecf69cae 100644 (file)
@@ -24,6 +24,8 @@
  *)
 
 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 ->
+   string list *
+    ((string -> CicTextualParser0.uri option) -> (Cic.metasenv * Cic.term))