]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug in detection of too polymorphic types partially fixed (see comment).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Nov 2007 15:14:23 +0000 (15:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Nov 2007 15:14:23 +0000 (15:14 +0000)
helm/software/components/cic_exportation/cicExportation.ml

index 9296b7bb05d260fd4429147b12c354104070a95c..c975ff11e8fb35ff92b192e698611f300af86431 100644 (file)
@@ -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