Missing whd.

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 8e7cb7c21226de2ac743f3ef0548f7a7b16f1011..096834d40fbddd87998d31e94656b45947de40f7 100644 (file)
--- 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