X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fnum.ml;h=aa9338c4c8d2d777fa45c5d0b74a85c376032dc7;hb=eeb6d213aac0f064babcb31ad6250be842d952b5;hp=1e630f4c6f43e24ca3e0c8557a8c59b3185cc0e5;hpb=b277f630cb63b40ae983282ea81ffefe288d3e8f;p=fireball-separation.git

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 1e630f4..aa9338c 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -295,8 +295,8 @@ let eta_compare x y =
   | `Pacman, `Pacman -> 0
   | `Lam _, `N _ -> -1
   | `N _, `Lam _ -> 1
-  | `Bottom, `Lam(_,t) -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux `Bottom t
-  | `Lam(_,t), `Bottom -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux t `Bottom
+  | `Bottom, `Lam(_,t) -> -1
+  | `Lam(_,t), `Bottom ->  1
   | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
   | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
   | t2, `Lam(_,t1) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))