From b285ae14dec63e8fc3d82813742ca69e5eb3a9a0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 17 May 2008 15:05:41 +0000 Subject: [PATCH] Missing whd. --- helm/software/components/ng_kernel/oCic2NCic.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 8e7cb7c21..096834d40 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -740,7 +740,8 @@ let cook mode vars t = let is_proof_irrelevant context ty = match - fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph) + CicReduction.whd context + (fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)) with Cic.Sort Cic.Prop -> true | Cic.Sort _ -> false -- 2.39.2