+
+(* adjusting the inferrable arguments that do not occur in the goal *********)
+
+let adjust c vs ?goal classes =
+ let list_xmap2 map l1 l2 =
+ let rec aux a = function
+ | hd1 :: tl1, hd2 :: tl2 -> aux (map hd1 hd2 :: a) (tl1,tl2)
+ | _, l2 -> List.rev_append l2 a
+ in
+ List.rev (aux [] (l1, l2))
+ in
+ let map where what (i, b) =
+ let what = H.cic what in
+ (i, b || not (H.occurs c ~what ~where))
+ in
+ match goal with
+ | None -> classes
+ | Some goal -> list_xmap2 (map goal) vs classes