get_subterm_with_head_and_args goes under lambdas

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index c78dde06e164a5be83be6e033095adae788271dd..0edd1b2586ee5dfee7141b8b59aff2901b3c1255 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -135,15 +135,16 @@ print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t
 ;;\r
 \r
 let get_subterm_with_head_and_args hd_var n_args =\r
- let rec aux = function\r
- | V _ | L _ | B | P -> None\r
+ let rec aux lev = function\r
+ | V _ | B | P -> None\r
+ | L t -> aux (lev+1) t\r
  | A(t1,t2) as t ->\r
-   if head_of_inert t1 = hd_var && n_args <= 1 + args_no t1\r
-    then Some t\r
-    else match aux t2 with\r
-    | None -> aux t1\r
+   if head_of_inert t1 = hd_var + lev && n_args <= 1 + args_no t1 (* why `1+' ?*)\r
+    then Some (lift ~-lev t)\r
+    else match aux lev t2 with\r
+    | None -> aux lev t1\r
     | Some _ as res -> res\r
- in aux\r
+ in aux 0\r
 ;;\r
 \r
 (* let rec simple_explode p =\r