From 9d6f485d270c2c60b5eb80bace1ae85b24a8e0fb Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 11 Jun 2018 11:54:49 +0200
Subject: [PATCH] Code simplication & fix

j+1 was j
---
 ocaml/simple.ml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

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
 ;;
 
-- 
2.39.2