]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Code simplication & fix
authoracondolu <andrea.condoluci@unibo.it>
Mon, 11 Jun 2018 09:54:49 +0000 (11:54 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 11 Jun 2018 09:54:49 +0000 (11:54 +0200)
j+1 was j

ocaml/simple.ml

index 7c372cbe7191c71c0fe8749b543cda39d1794501..5c158b3b0b400c09b6dca7ff3bf0d1916fb8afe1 100644 (file)
@@ -279,15 +279,13 @@ let find_eta_difference p t =
 \r
 let compute_max_lambdas_at hd_var j =\r
  let rec aux hd = function\r
- | A(t1,t2) ->\r
+ | A(t1,t2) -> max (max (aux hd t1) (aux hd t2))\r
     (if get_inert t1 = (V hd, j)\r
-      then max ( (*FIXME*)\r
-       if is_inert t2 && let hd', j' = get_inert t2 in hd' = V hd\r
-        then let hd', j' = get_inert t2 in j - j'\r
-        else no_leading_lambdas hd_var j t2)\r
-      else id) (max (aux hd t1) (aux hd t2))\r
+      then no_leading_lambdas hd (j+1) t2\r
+      else 0)\r
  | L(t,_) -> aux (hd+1) t\r
- | V _ | C -> 0\r
+ | V _\r
+ | C -> 0\r
  in aux hd_var\r
 ;;\r
 \r