]> matita.cs.unibo.it Git - helm.git/commitdiff
Missing whd.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 15:05:41 +0000 (15:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 15:05:41 +0000 (15:05 +0000)
helm/software/components/ng_kernel/oCic2NCic.ml

index 8e7cb7c21226de2ac743f3ef0548f7a7b16f1011..096834d40fbddd87998d31e94656b45947de40f7 100644 (file)
@@ -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