diff options
Diffstat (limited to 'test/KB')
| -rw-r--r-- | test/KB/kb.ml | 2 | ||||
| -rw-r--r-- | test/KB/terms.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/test/KB/kb.ml b/test/KB/kb.ml index 52c9e8d1eb..329c0b5915 100644 --- a/test/KB/kb.ml +++ b/test/KB/kb.ml @@ -168,7 +168,7 @@ let kb_completion greater = let ek = (rk.lhs, rk.rhs) in process failures (k,l) (mutual_critical_pairs el (rename rl.numvars ek)) - with Not_found -> next_criticals failures (k+1,l) + with Not_found -> next_criticals failures (k+1,l) with Not_found -> next_criticals failures (1,l+1) in process in kbrec diff --git a/test/KB/terms.ml b/test/KB/terms.ml index 493bfb2625..9f9acffbc6 100644 --- a/test/KB/terms.ml +++ b/test/KB/terms.ml @@ -63,7 +63,7 @@ let matching term1 term2 = else (v, t2) :: subst | Term(op1,sons1), Term(op2,sons2) -> - if op1 = op2 + if op1 = op2 then List.fold_left2 match_rec subst sons1 sons2 else failwith "matching" | _ -> failwith "matching" in @@ -92,7 +92,7 @@ let rec unify term1 term2 = else [n2, term1] | Term(op1,sons1), Term(op2,sons2) -> if op1 = op2 then - List.fold_left2 (fun s t1 t2 -> compsubst (unify (substitute s t1) + List.fold_left2 (fun s t1 t2 -> compsubst (unify (substitute s t1) (substitute s t2)) s) [] sons1 sons2 else failwith "unify" @@ -117,7 +117,7 @@ let rec pretty_term = function end else begin print_string oper; match sons with - [] -> () + [] -> () | t::lt -> print_string "("; pretty_term t; List.iter (fun t -> print_string ","; pretty_term t) lt; |