OEIS sequence identifier found for P(n)

[helm.git] / helm / software / matita / applyTransformation.ml

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index ac044cefed05b15bc5810636555893e02101b5a1..e741ed70c4ba8c79f1f88488057bd51522487b27 100644 (file)
--- 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 ->