Partial porting to V8 URIs.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 3f504ab7957426aa193e81240336dec3a567bbd3..137f786ab1fc003e7432605ee82116a0e9d6093c 100644 (file)
--- 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 =