+ let all_separated = List.for_all (fun (_, lst) -> List.length lst = 1 || List.for_all (fun (_,(t,_)) -> is_var t) lst) p.matches in\r
+ all_separated && List.exists ((=) B) p.div\r
+;;\r
+\r
+let free_vars p t =\r
+ let rec aux level = function\r
+ | V v -> if v >= level then [v] else []\r
+ | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
+ | L t -> aux (level+1) t\r
+ | LM(ts,_,id) -> (List.concat (List.map (aux level) ts)) @ (\r
+ let lst = List.assoc id p.matches in\r
+ List.concat (List.map (fun (_,(t1,t2)) -> (aux 0 t1) @ (aux 0 t2)) lst)\r
+ )\r
+ | B -> []\r
+ | P -> []\r
+ in Util.sort_uniq (aux 0 t)\r
+;;\r
+\r
+let visible_vars p t =\r
+ let rec aux = function\r
+ | V v -> [v]\r
+ | A(t1,t2) -> (aux t1) @ (aux t2)\r
+ | L t -> []\r
+ | LM(ts,_,id) -> (List.concat (List.map aux ts)) @ (\r
+ let lst = List.assoc id p.matches in\r
+ List.concat (List.map (fun (_,(t1,t2)) -> (aux t1) @ (aux t2)) lst)\r
+ )\r
+ | B -> []\r
+ | P -> []\r
+ in Util.sort_uniq (aux t)\r
+;;\r
+\r
+let forget_variable var p =\r
+ let p', div = subst_many true (var, P) p p.div in\r
+ let p = {p' with conv=p.conv} in\r
+ let p, conv = subst_many false (var, B) p p.conv in\r
+ let p, matches = subst_in_matches (var, B) p p.matches in\r
+ {p with div; conv; matches; sigma=p.sigma}\r
+;;\r
+let rec remove_divergent_discriminators p =\r
+ let f = fun (b,(t,_)) -> b && (t = B || is_lambda t) in\r
+ try\r
+ let v,l = List.find (fun (_,lst) -> List.exists f lst) p.matches in\r
+ let (_,(_,c)) as entry = List.find f l in\r
+ let l = List.filter ((<>) entry) l in\r
+ let matches = List.map (fun (v', l') -> v', if v' = v then l else l') p.matches in\r
+ let vars = free_vars p c in\r
+ let p = {p with matches} in\r
+ List.fold_right forget_variable vars p\r
+ with Not_found -> p\r