-let infer env sign current active =
- let rec infer_negative current = function
- | [] -> [], []
- | (Negative, _)::tl -> infer_negative current tl
- | (Positive, equality)::tl ->
- let res = superposition_left env current equality in
- let neg, pos = infer_negative current tl in
- res @ neg, pos
-
- and infer_positive current = function
- | [] -> [], []
- | (Negative, equality)::tl ->
- let res = superposition_left env equality current in
- let neg, pos = infer_positive current tl in
- res @ neg, pos
- | (Positive, equality)::tl ->
- let maxm, res = superposition_right !maxmeta env current equality in
- let maxm, res' = superposition_right maxm env equality current in
- maxmeta := maxm;
- let neg, pos = infer_positive current tl in
-
-(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
-(* (string_of_equality ~env current) (string_of_equality ~env equality) *)
-(* (String.concat "\n" (List.map (string_of_equality ~env) res)); *)
-(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
-(* (string_of_equality ~env equality) (string_of_equality ~env current) *)
-(* (String.concat "\n" (List.map (string_of_equality ~env) res')); *)
-
- neg, res @ res' @ pos
- in