+ and check_exp_named_subst uri ~logger ~subst context ens ugraph =
+ let params =
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match obj with
+ Cic.Constant (_,_,_,params,_) -> params
+ | Cic.Variable (_,_,_,params,_) -> params
+ | Cic.CurrentProof (_,_,_,_,params,_) -> params
+ | Cic.InductiveDefinition (_,params,_,_) -> params
+ ) in
+ let rec check_same_order params ens =
+ match params,ens with
+ | _,[] -> ()
+ | [],_::_ ->
+ raise (TypeCheckerFailure (lazy "Bad explicit named substitution"))
+ | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' ->
+ check_same_order tl tl'
+ | _::tl,l -> check_same_order tl l
+ in