]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
First commit towards more powerful disambiguation possibilities, where
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParserContext.mli
index 23ad4af115ef8edd9205c1a2298d4db3dd81aec3..0b8871ee83aeb9a271ad280c45360380cb7d1fd9 100644 (file)
@@ -27,7 +27,5 @@ val main :
   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
+   CicTextualParser0.interpretation_domain_item list *
+    (CicTextualParser0.interpretation -> (Cic.metasenv * Cic.term))