]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualParser0.ml
Interface improvement (???): the Check button has been moved to a brand new
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser0.ml
index 0a841473474275adee71d1b89f11a3f8b47eeaf5..62bf7f23cd0980e1a7ce579ac19abf4bfb270da6 100644 (file)
 
 exception Eof;;
 
-let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");;
+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);;