]> matita.cs.unibo.it Git - helm.git/commitdiff
CProp uri fixed
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 14 Oct 2009 08:51:13 +0000 (08:51 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 14 Oct 2009 08:51:13 +0000 (08:51 +0000)
helm/software/components/ng_library/oCic2NCic.ml

index 1cf194a4c7e91eb970e0eac10f98273ae6c578dc..7225ea2a44198690e17e93ab366f9907352dccca 100644 (file)
@@ -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 =