-(* debug_print (lazy "First Order UnificationFailure during delift") ;
-debug_print(lazy (sprintf
- "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
- (ppterm subst t)
- (String.concat "; "
- (List.map
- (function Some t -> ppterm subst t | None -> "_") l
- )))); *)
- let msg = (lazy (sprintf
- "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
- (ppterm ~metasenv subst t)
- (String.concat "; "
- (List.map
- (function Some t -> ppterm ~metasenv subst t | None -> "_")
- l))))
+ let msg = (lazy (Printf.sprintf
+ ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
+ "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst
+ ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv
+ ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
+ shift) (NCicUtils.expand_local_context lc))))))