Removed useless `isdiv' flag

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 8066a3d79f76e5a845cdaa67de2212afdcf14834..c78dde06e164a5be83be6e033095adae788271dd 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -98,19 +98,19 @@ let rec args_no = function
  | _ -> assert false\r
 ;;\r
 \r
-let rec subst level delift fromdiv sub =\r
+let rec subst level delift sub =\r
  function\r
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
- | L t -> L (subst (level + 1) delift fromdiv sub t)\r
+ | L t -> L (subst (level + 1) delift sub t)\r
  | A (t1,t2) ->\r
-  let t1 = subst level delift fromdiv sub t1 in\r
-  let t2 = subst level delift fromdiv sub t2 in\r
-  if t1 = B || t2 = B then B else mk_app fromdiv t1 t2\r
+  let t1 = subst level delift sub t1 in\r
+  let t2 = subst level delift sub t2 in\r
+  if t1 = B || t2 = B then B else mk_app t1 t2\r
  | B -> B\r
  | P -> P\r
-and mk_app fromdiv t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
+and mk_app t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
  | B | _ when t2 = B -> B\r
- | L t1 -> subst 0 true fromdiv (0, t2) t1\r
+ | L t1 -> subst 0 true (0, t2) t1\r
  | t1 -> A (t1, t2)\r
 and lift n =\r
  let rec aux n' =\r
@@ -127,8 +127,8 @@ let subst = subst 0 false;;
 let subst_in_problem (sub: var * t) (p: problem) =\r
 print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
  let p = {p with stepped=(fst sub)::p.stepped} in\r
- let conv = subst false sub p.conv in\r
- let div = subst true sub p.div in\r
+ let conv = subst sub p.conv in\r
+ let div = subst sub p.div in\r
  let p = {p with div; conv} in\r
  (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
  {p with sigma=sub::p.sigma}\r
@@ -204,7 +204,7 @@ let parse strs =
   let rec aux level = function\r
   | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
   | Parser_andrea.App (t1, t2) ->\r
-   if level = 0 then mk_app false (aux level t1) (aux level t2)\r
+   if level = 0 then mk_app (aux level t1) (aux level t2)\r
     else A(aux level t1, aux level t2)\r
   | Parser_andrea.Var v -> V v\r
   in let (tms, free) = Parser_andrea.parse_many strs\r
@@ -288,7 +288,7 @@ let rec auto p =
  let n_args = args_no p.div in\r
  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
  | None ->\r
-    (try let p = eat p in problem_fail p "Auto did not complete the problem"  with Done _ -> ())\r
+    (try problem_fail (eat p) "Auto did not complete the problem"  with Done _ -> ())\r
  | Some t ->\r
   let j = find_eta_difference p t n_args - 1 in\r
   let k = max\r