+ and visit_exp_named_subst context uri exp_named_subst =
+ let uris_and_types =
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Constant (_,_,_,params)
+ | Cic.CurrentProof (_,_,_,_,params)
+ | Cic.Variable (_,_,_,params)
+ | Cic.InductiveDefinition (_,params,_) ->
+ List.map
+ (function uri ->
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Variable (_,None,ty,_) -> uri,ty
+ | _ -> assert false (* the theorem is well-typed *)
+ ) params
+ in
+ let rec check uris_and_types subst =
+ match uris_and_types,subst with
+ _,[] -> []
+ | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
+ ignore (type_of_aux context t (Some ty)) ;
+ let tytl' =
+ List.map
+ (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
+ in
+ check tytl' substtl
+ | _,_ -> assert false (* the theorem is well-typed *)
+ in
+ check uris_and_types exp_named_subst
+