- ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
- NCic.LetIn ("clause_" ^ string_of_int id,
- extract amount [] lit,
- (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
- aux true ((id,([],lit))::seen) (id::tl)))
+ let lit = Subst.apply_subst subst lit in
+ let eq_ty = extract amount [] lit in
+ let refl = mk_refl eq_ty in
+ (*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
+ (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
+ aux true ((id,([],lit))::seen) (id::tl))) *)
+ NCicSubstitution.subst
+ ~avoid_beta_redexes:true ~no_implicit:false refl
+ (aux true ((id,([],lit))::seen) (id::tl))