X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=225269b70fe101eaccf2ed9373c4c1a1634a0e92;hb=b68e52f889215ce2c21c3d771f59b2d2057d53c1;hp=6b78512bd6f9203f29f6405690cdca6dfb655b34;hpb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 6b78512bd..225269b70 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -16,10 +16,7 @@ module Ref = NReference
 let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
 
 let mk_type n = 
-  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 mk_cprop n = 
@@ -258,7 +255,7 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ "  " ^ CicPp.ppterm arity);*)
   match CicReduction.whd context tty with
      Cic.MutInd (_,_,ens) -> ens,[]
    | Cic.Appl (Cic.MutInd (_,_,ens)::args) ->
-      ens,fst (HExtlib.split_nth "ON 1" leftno args)
+      ens,fst (HExtlib.split_nth leftno args)
    | _ -> assert false
  in
   let rec aux n irl context outsort =
@@ -871,3 +868,11 @@ let convert_term uri ctx t =
    aux false [] [] 0 uri t
 ;;
 *)
+
+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
+;;