X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser0.ml;h=7a53057e24729653669fd68f4de98820bc683ac2;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=fe4bf062346c95b9cf29eaeb692871f4fccab3fd;hpb=691f90554fe985a5ef67a7e82fb684ab10024fac;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index fe4bf0623..7a53057e2 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -24,11 +24,25 @@
  *)
 
 exception Eof;;
+exception LexerFailure of string;;
+
+type uri =
+   ConUri of UriManager.uri
+ | VarUri of UriManager.uri
+ | IndTyUri of UriManager.uri * int
+ | IndConUri of UriManager.uri * int * int
+;;
+
+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 current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");;
 let binders = ref ([] : (Cic.name option) list);;
 let metasenv = ref ([] : Cic.metasenv);;
-let locate_object = ref ((fun _ -> None):string->Cic.term option);;
-
-let set_locate_object f =
-   locate_object := f