X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_exportation%2FcicExportation.ml;h=c975ff11e8fb35ff92b192e698611f300af86431;hb=9cb292942b04f5e5e529bd4294df54dc83fa399f;hp=9296b7bb05d260fd4429147b12c354104070a95c;hpb=d75c0ceca138ed1a29ea9a623e28051c03beb373;p=helm.git

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 9296b7bb0..c975ff11e 100644
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -238,9 +238,10 @@ let rec pp ~in_type t context =
         "unit (* TOO POLYMORPHIC TYPE *)"
        else (
        let needs_obj_magic =
-        match ty with
+        (* BUG HERE: we should consider also the right parameters *)
+        match CicReduction.whd context ty with
            Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
-         | _ -> assert false
+         | _ -> false (* it can be a Rel, e.g. in *_rec *)
        in
        (match analyze_term context te with
            `Type -> assert false