This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / grafite_engine / nCicCoercDeclaration.ml

diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
index a26d5ec7c267b986449b9ae55646bbc9660c40ee..cf3c127b95371d9536bb0d7a3a3c9e5e7d265c5e 100644 (file)
--- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
@@ -174,7 +174,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
 let fresh_uri status prefix suffix = 
   let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
   let rec diverge u i =
-    if NCicLibrary.aliases_of u = [] then u
+    if NCicLibrary.aliases_of status u = [] then u
     else diverge (mk ("__" ^ string_of_int i)) (i+1)
   in
    diverge (mk "") 0
@@ -295,7 +295,9 @@ let record_ncoercion =
   ~refresh_uri_in_reference ~alias_only status
  =
   if not alias_only then
-   List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
+   List.fold_right 
+    (aux ~refresh_uri_in_term:(refresh_uri_in_term
+     (status:>NCicEnvironment.status))) l status
   else
    status
  in