From 86946c16c60b3d3c5f0574ba380b109d9338bcc7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Nov 2007 15:14:23 +0000 Subject: [PATCH] Bug in detection of too polymorphic types partially fixed (see comment). --- helm/software/components/cic_exportation/cicExportation.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.39.2