X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=cf3c127b95371d9536bb0d7a3a3c9e5e7d265c5e;hb=dab25d81b789fb8430ef76f2dd77970c2c410048;hp=f1b051d46f229915a02bdfe15daaf9f238a0a3d0;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
index f1b051d46..cf3c127b9 100644
--- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
@@ -9,6 +9,9 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
+(* TODO: all newast's must be returned to the caller in some way
+ * e.g. modifying the status? *)
+
 (* let debug s = prerr_endline (Lazy.force s) ;;*)
 let debug _ = ();;
 
@@ -171,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
@@ -292,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