| ((uri,t) as subst)::tl ->
let typeofvar =
CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: this test should not exist
(match CicEnvironment.get_cooked_obj ~trust:false uri with
Cic.Variable (_,Some bo,_,_) ->
raise
("Unknown variable definition:" ^
UriManager.string_of_uri uri))
) ;
+*)
let typeoft = type_of_aux context t in
if CicReduction.are_convertible context typeoft typeofvar then
check_exp_named_subst_aux (substs@[subst]) tl