X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser0.ml;h=e75f61bd78212f2e97b4b61adeb380f0a9c9cf25;hb=19ebb626366e7e8f2ff906fd410a2427d375ff5d;hp=fab36396087cb41a1ab691e71a9c28f4d4d3a6fd;hpb=a3b863935bfacffb76ccc913c737be53b840ffe4;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index fab363960..e75f61bd7 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -32,9 +32,15 @@ type uri =
  | IndConUri of UriManager.uri * int * int
 ;;
 
-type interp_codomain =
+type interpretation_domain_item =
+   Id of string
+ | Symbol of string * (string * (interpretation -> Cic.term)) list
+and interpretation_codomain_item =
    Uri of uri
  | Implicit
+ | Term of (interpretation -> Cic.term)
+and interpretation =
+ interpretation_domain_item -> interpretation_codomain_item option
 ;;
 
 let binders = ref ([] : (Cic.name option) list);;