- let rec traverse_list i l1 l2 = match l1, l2 with
- | [], [] ->
- T.then_ ~start:(clear_term first_time context term)
- ~continuation:(continuation ~map:id)
- | hd1 :: tl1, hd2 :: tl2 ->
- if are_convertible hd1 hd2 metasenv context then
- traverse_list (succ i) tl1 tl2
- else
- injection_tac ~i ~term ~continuation:
- (qnify_tac ~first_time:false ~term ~continuation)
- | _ -> assert false
+ let rec traverse_list first_time i l1 l2 =
+ match l1, l2 with
+ | [], [] ->
+ fun ~map:aftermap ->
+ T.then_ ~start:(clear_term first_time context term)
+ ~continuation:(after continuation aftermap map)
+ | hd1 :: tl1, hd2 :: tl2 ->
+ if are_convertible hd1 hd2 metasenv context then
+ traverse_list first_time (succ i) tl1 tl2
+ else
+ injection_tac ~i ~term ~continuation:
+ (traverse_list false (succ i) tl1 tl2)
+ | _ -> assert false