+
+and get_relevance ~subst context = function
+ | C.Const r ->
+ let relevance = E.get_relevance r in
+ (match r with
+ | Ref.Ref (_,Ref.Con (_,_,lno)) ->
+ let _,relevance = HExtlib.split_nth lno relevance in
+ HExtlib.mk_list false lno @ relevance
+ | _ -> relevance)
+ | t ->
+ let ty = typeof ~subst ~metasenv:[] context t in
+ let rec aux context = function
+ | C.Prod (name,so,de) ->
+ let sort = typeof ~subst ~metasenv:[] context so in
+ (match sort with
+ | C.Sort C.Prop -> false::(aux ((name,(C.Decl so))::context) de)
+ | C.Sort _ -> true::(aux ((name,(C.Decl so))::context) de)
+ | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
+ "Prod: the type %s of the source of %s is not a sort"
+ (PP.ppterm ~subst ~metasenv:[] ~context sort)
+ (PP.ppterm ~subst ~metasenv:[] ~context so)))))
+ | _ -> []
+ in aux context ty