Improved definition of eta_eq

Probably still not just right

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 079774e5ac67e5c53feaa53eca9e7e622dd77c76..34f9f72efa14cd7cf614eb316be2f5c1894c3578 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -23,8 +23,11 @@ let rec is_stuck = function
 ;;\r
 \r
 let eta_eq' =\r
- let rec aux l1 l2 t1 t2 = match t1, t2 with\r
-  | _, _ when is_stuck t1 || is_stuck t2 -> true\r
+ let rec aux l1 l2 t1 t2 =\r
+  let stuck1, stuck2 = is_stuck t1, is_stuck t2 in\r
+  match t1, t2 with\r
+  | _, _ when not stuck1 && stuck2 -> false\r
+  | _, _ when stuck1 -> true\r
   | L t1, L t2 -> aux l1 l2 (fst t1) (fst t2)\r
   | L t1, t2 -> aux l1 (l2+1) (fst t1) t2\r
   | t1, L t2 -> aux (l1+1) l2 t1 (fst t2)\r