X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=e741ed70c4ba8c79f1f88488057bd51522487b27;hb=05ebdd213d5968b9f0eeaa01e4f9aac33ef86c7c;hp=ac044cefed05b15bc5810636555893e02101b5a1;hpb=9e010764b6de0d8a268a6ecb83e8e90246bee129;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index ac044cefe..e741ed70c 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -280,7 +280,7 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
 	in
 	if real then do_it obj else
 	let newuri = discharge_uri style uri in
-	let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in
+	let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in
 	do_it obj
       with
          | TC.TypeCheckerFailure s ->