Huge commit with several changes:

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 2738b1c901835183078c7a24b0f3470475f13f02..225269b70fe101eaccf2ed9373c4c1a1634a0e92 100644 (file)
--- 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 = 
@@ -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
+;;