+let mk_cprop n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+;;
+
+let is_proof_irrelevant context ty =
+ match
+ CicReduction.whd context
+ (fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph))
+ with
+ Cic.Sort Cic.Prop -> true
+ | Cic.Sort _ -> false
+ | _ -> assert false
+;;
+
+exception InProp;;
+
+let get_relevance ty =
+ let rec aux context ty =
+ match CicReduction.whd context ty with
+ Cic.Prod (n,s,t) ->
+ not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t
+ | _ -> []
+ in aux [] ty
+(* | ty -> if is_proof_irrelevant context ty then raise InProp else []
+ in
+ try aux [] ty
+ with InProp -> []*)
+;;
+