X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=4522a0a1a917855a8aed045d35b1eaa52d753e94;hb=d4f2d4c1a4784f84aa27e1bb96b8b377a6553c65;hp=7cc5644d99c54ea74e0b041cbd4963cae07daf4e;hpb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;p=helm.git

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 7cc5644d9..4522a0a1a 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -282,14 +282,16 @@ 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
+ =
+   List.fold_right (aux ~refresh_uri_in_term) l
  in
   GrafiteTypes.Serializer.register#run "ncoercion" aux_l 
 ;;