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