Fixed: was using compare in place of eta_eq

[fireball-separation.git] / ocaml / lambda4.ml

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 97228ed0a0a87a98be484a4bc9a62a992558f9a4..c79cade6383dccc699c3ea591c6216237de477ff 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -111,7 +111,7 @@ let simple_expand_match ps =
     (try
        (match u with
          | #i_n_var as u ->
-            let i = index_of (lift (-level) u) (ps :> nf list) in (* can raise Not_found *)
+            let i = index_of ~eq:eta_eq (lift (-level) u) (ps :> nf list) in (* can raise Not_found *)
             let t = cast_to_i_num_var (mk_match (`N i) v bs_lift bs (args :> nf list)) in
             if t <> torig then
              aux_i_num_var level t