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