- if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
- else
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
let t, _ = aux true oc auxc 0 uri ty in
(name_of s, NCic.Def (t,ty)) :: nc,
Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc, e :: oc
let t, _ = aux true oc auxc 0 uri ty in
(name_of s, NCic.Def (t,ty)) :: nc,
Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc, e :: oc
+*)
+
+let reference_of_oxuri u =
+ let t = CicUtil.term_of_uri u in
+ let t',l = convert_term (UriManager.uri_of_string "cic:/dummy/dummy.con") t in
+ match t',l with
+ NCic.Const nref, [] -> nref
+ | _,_ -> assert false
+;;