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