From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Nov 2007 15:14:23 +0000 (+0000)
Subject: Bug in detection of too polymorphic types partially fixed (see comment).
X-Git-Tag: make_still_working~5896
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=86946c16c60b3d3c5f0574ba380b109d9338bcc7;p=helm.git

Bug in detection of too polymorphic types partially fixed (see comment).
---

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 9296b7bb0..c975ff11e 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/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