type_of_aux ~logger
((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
in
- (CicSubstitution.subst s ty1),ugraph2
+ (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
| C.Appl (he::tl) when List.length tl > 0 ->
let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
let tlbody_and_type,ugraph2 =
begin
CicReduction.fdebug := -1 ;
eat_prods ~subst context
- (CicSubstitution.subst hete t) tl ugraph1
+ (CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+ tl ugraph1
(*TASSI: not sure *)
end
else