The interpretation function can now return also "Implicit".

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser0.ml

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index 62bf7f23cd0980e1a7ce579ac19abf4bfb270da6..fab36396087cb41a1ab691e71a9c28f4d4d3a6fd 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -32,5 +32,10 @@ type uri =
  | IndConUri of UriManager.uri * int * int
 ;;
 
+type interp_codomain =
+   Uri of uri
+ | Implicit
+;;
+
 let binders = ref ([] : (Cic.name option) list);;
 let metasenv = ref ([] : Cic.metasenv);;