X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_library%2FoCic2NCic.ml;h=7225ea2a44198690e17e93ab366f9907352dccca;hb=cd415135f0bcf53f10ed7649fcacc3247bc7a3f1;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..7225ea2a4 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 =