From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 29 May 2018 09:03:42 +0000 (+0200)
Subject: Removed useless `isdiv' flag
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7ed79cb0dc07847da37b68af96f13223ce71079;p=fireball-separation.git

Removed useless `isdiv' flag
---

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