From: Claudio Sacerdoti Coen 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: 0.4.95@7852~47 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9cb292942b04f5e5e529bd4294df54dc83fa399f;p=helm.git Bug in detection of too polymorphic types partially fixed (see comment). --- 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