From d88c6bdb650d69ffccac2031cecf7a50cd7e6917 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 Oct 2009 08:51:13 +0000 Subject: [PATCH] CProp uri fixed --- helm/software/components/ng_library/oCic2NCic.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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 = -- 2.39.2