X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser0.ml;h=62bf7f23cd0980e1a7ce579ac19abf4bfb270da6;hb=a9e833b37216b225262450fd4e3fa5bf79ae4c3a;hp=e89c00d22bff826ba72c507b2c01a9ef76f28187;hpb=818c90057de4f3ca2e1971b267549fe146b89b6f;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index e89c00d22..62bf7f23c 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -25,5 +25,12 @@
 
 exception Eof;;
 
-let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");;
-let binders = ref ([] : Cic.name list);;
+type uri =
+   ConUri of UriManager.uri
+ | VarUri of UriManager.uri
+ | IndTyUri of UriManager.uri * int
+ | IndConUri of UriManager.uri * int * int
+;;
+
+let binders = ref ([] : (Cic.name option) list);;
+let metasenv = ref ([] : Cic.metasenv);;