Fix: conv : x:min_int (.... y:1 ...) y was not considered for stepping

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 35f03ca8bf4af09dc6bde54560cc789edbff12e7..570691e1be16101622515e0d8c55a70bceda31bc 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -499,8 +499,12 @@ let auto_instantiate (n,p) =
        fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
       ) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
      (match heads with
-         [] ->
-         assert false
+         [] -> (
+          try
+           fst (List.find (((<) 0) ++ snd) (concat_map free_vars' (p.conv :> nf list)))
+          with
+           Not_found -> assert false
+          )
        | x::_ ->
           prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
           x)