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 788fe5983357dddd15e531364f8203664570ed86..ed43936638020efe31958242c0edd27b11834f60 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -126,7 +126,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