From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 11 Jun 2018 09:54:49 +0000 (+0200)
Subject: Code simplication & fix
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=9d6f485d270c2c60b5eb80bace1ae85b24a8e0fb;p=fireball-separation.git

Code simplication & fix

j+1 was j
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 7c372cb..5c158b3 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -279,15 +279,13 @@ let find_eta_difference p t =
 
 let compute_max_lambdas_at hd_var j =
  let rec aux hd = function
- | A(t1,t2) ->
+ | A(t1,t2) -> max (max (aux hd t1) (aux hd t2))
     (if get_inert t1 = (V hd, j)
-      then max ( (*FIXME*)
-       if is_inert t2 && let hd', j' = get_inert t2 in hd' = V hd
-        then let hd', j' = get_inert t2 in j - j'
-        else no_leading_lambdas hd_var j t2)
-      else id) (max (aux hd t1) (aux hd t2))
+      then no_leading_lambdas hd (j+1) t2
+      else 0)
  | L(t,_) -> aux (hd+1) t
- | V _ | C -> 0
+ | V _
+ | C -> 0
  in aux hd_var
 ;;