- let hd, n_args = get_inert p.div in\r
- match hd with\r
- | C | L _ | A _ -> assert false\r
- | V hd_var ->\r
- let tms = get_subterms_with_head hd_var p.conv in\r
- if List.exists (fun t -> snd (get_inert t) >= n_args) tms\r
- then (\r
- (* let tms = List.sort (fun t1 t2 -> - compare (snd (get_inert t1)) (snd (get_inert t2))) tms in *)\r
- try_all "no similar terms" (fun t ->\r
+ match p.div with\r
+ | L(div,g) -> (* case p.div is an abstraction *)\r
+ let f l t = fst (subst' 0 true (0, C) t) :: l in\r
+ (* the `fst' above is because we can ignore the\r
+ garbage generated by the subst, because substituting\r
+ C does not create redexes and thus no new garbage is activated *)\r
+ let tms = List.fold_left f [] (div::g) in\r
+ try_all "auto.L"\r
+ (fun div -> aux {p with div}) tms\r
+ | _ -> (\r
+ if is_constant p.div (* case p.div is rigid inert *)\r
+ then try_all "auto.C"\r
+ (fun div -> aux {p with div}) (args_of_inert p.div)\r
+ else (* case p.div is flexible inert *)\r
+ let hd, n_args = get_inert p.div in\r
+ match hd with\r
+ | C | L _ | A _ -> assert false\r
+ | V hd_var ->\r
+ let tms = get_subterms_with_head hd_var p.conv in\r
+ if List.exists (fun t -> snd (get_inert t) >= n_args) tms\r
+ then (\r
+ (* let tms = List.sort (fun t1 t2 -> - compare (snd (get_inert t1)) (snd (get_inert t2))) tms in *)\r
+ try_all "no similar terms" (fun t ->\r