New CicTextualParser: it now returns (approximately) a couple

[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..23ad4af115ef8edd9205c1a2298d4db3dd81aec3 100644 (file)
--- 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) ->
-   (Lexing.lexbuf  -> CicTextualParser.token) -> Lexing.lexbuf ->
-     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