The interpretation function can now return also "Implicit".

[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 c83ac03f8b1df4beeb2cfccfa3dad241ecf69cae..c95e7e2e76b90b25d03f0c31e4f3e1f5ce4a6125 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
@@ -28,4 +28,5 @@ val main :
   metasenv:Cic.metasenv ->
   (Lexing.lexbuf  -> CicTextualParser.token) -> Lexing.lexbuf ->
    string list *
-    ((string -> CicTextualParser0.uri option) -> (Cic.metasenv * Cic.term))
+    ((string -> CicTextualParser0.interp_codomain option) ->
+      (Cic.metasenv * Cic.term))