X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_library%2FoCic2NCic.ml;h=50b3207e89d2114167969a792250e7f918eeefb7;hb=61d514611fc8434164c4275e7b59f81617104ef3;hp=1cf194a4c7e91eb970e0eac10f98273ae6c578dc;hpb=7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5;p=helm.git

diff --git a/helm/software/components/ng_library/oCic2NCic.ml b/helm/software/components/ng_library/oCic2NCic.ml
index 1cf194a4c..50b3207e8 100644
--- a/helm/software/components/ng_library/oCic2NCic.ml
+++ b/helm/software/components/ng_library/oCic2NCic.ml
@@ -20,10 +20,7 @@ let mk_type n =
 ;;
 
 let mk_cprop n = 
-  if n = 0 then 
-    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
-  else
-    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let is_proof_irrelevant context ty =
@@ -880,5 +877,7 @@ let reference_of_oxuri u =
 NCicCoercion.set_convert_term convert_term;;
 Ncic2astMatcher.set_reference_of_oxuri reference_of_oxuri;;
 NCicDisambiguate.set_reference_of_oxuri reference_of_oxuri;;
+(* Why should we set them here? 
 NCicBlob.set_reference_of_oxuri reference_of_oxuri;;
 NCicProof.set_reference_of_oxuri reference_of_oxuri;;
+*)