X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=137f786ab1fc003e7432605ee82116a0e9d6093c;hb=b3bfd6b249600b15552c890306a635aee30c2a74;hp=3f504ab7957426aa193e81240336dec3a567bbd3;hpb=ba2709d8c270e7f6ffbdb8bd3a192bc071407f03;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 3f504ab79..137f786ab 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -265,7 +265,7 @@ and weakly_positive context n nn uri te =
  let module C = Cic in
 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
   let dummy_mutind =
-   C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[])
+   C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
   in
   (*CSC mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy_mutind =