From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 17 May 2008 15:05:41 +0000 (+0000)
Subject: Missing whd.
X-Git-Tag: make_still_working~5182
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b285ae14dec63e8fc3d82813742ca69e5eb3a9a0;p=helm.git

Missing whd.
---

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