X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=e204422e35e973b3918b9b16cb471b4fe31ba5f4;hb=fe5542c1ce4e78d2ec4e9b39cfc4f06182555e99;hp=3cf07626531c37902cff53640451885386211997;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 3cf076265..e204422e3 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -133,7 +133,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
            (try 
             let metasenv,subst,status,src =
               GrafiteDisambiguate.disambiguate_nterm 
-                None status ctx [] [] ("",0,src) in
+                status None ctx [] [] ("",0,src) in
             let src = NCicUntrusted.apply_subst subst [] src in
             (* CHECK that the declared pattern matches the abstraction *)
             let _ = NCicUnification.unify status metasenv subst ctx ty src in
@@ -151,7 +151,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
   let status, tgt, arity = 
     let metasenv,subst,status,tgt =
       GrafiteDisambiguate.disambiguate_nterm 
-        None status [] [] [] ("",0,tgt) in
+        status None [] [] [] ("",0,tgt) in
     let tgt = NCicUntrusted.apply_subst subst [] tgt in
     (* CHECK che sia unificabile mancante *)
     let rec count_prod = function
@@ -282,25 +282,26 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
 ;;
 
 let record_ncoercion =
- let aux (name,t,s,d,p,a) ~refresh_uri_in_universe ~refresh_uri_in_term =
+ let aux (name,t,s,d,p,a) ~refresh_uri_in_term =
   let t = refresh_uri_in_term t in
   let s = refresh_uri_in_term s in
   let d = refresh_uri_in_term d in
    basic_index_ncoercion (name,t,s,d,p,a)
  in
- let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
-   List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
+ let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
+  ~refresh_uri_in_reference ~alias_only status
+ =
+  if not alias_only then
+   List.fold_right (aux ~refresh_uri_in_term) l status
+  else
+   status
  in
-  NCicLibrary.Serializer.register#run "ncoercion"
-   object(self : 'a NCicLibrary.register_type)
-    method run = aux_l 
-   end
+  GrafiteTypes.Serializer.register#run "ncoercion" aux_l 
 ;;
 
 let basic_eval_and_record_ncoercion infos status =
  let uris, cinfos, status = basic_eval_ncoercion infos status in
- let dump = record_ncoercion (infos::cinfos) :: status#dump in
-  status#set_dump dump, uris
+  NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
 ;;
 
 let basic_eval_and_record_ncoercion_from_t_cpos_arity 
@@ -314,17 +315,15 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity
    status,uris
 ;;
 
-let eval_ncoercion status name t ty (id,src) tgt = 
-
+let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = 
  let metasenv,subst,status,ty =
-  GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
+  GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
  assert (metasenv=[]);
  let ty = NCicUntrusted.apply_subst subst [] ty in
  let metasenv,subst,status,t =
-  GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
+  GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
-
  let status, src, tgt, cpos, arity = 
    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
  let status, uris =