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=0a841473474275adee71d1b89f11a3f8b47eeaf5;hpb=faf328f5779a7281c9c0588680b1b7bb89ae7640;p=helm.git diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml index 0a8414734..62bf7f23c 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml @@ -25,6 +25,12 @@ 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);;