From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 29 May 2018 09:03:53 +0000 (+0200)
Subject: get_subterm_with_head_and_args goes under lambdas
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0e626fb979562114f436e2f2173a1062d8bbc31;p=fireball-separation.git

get_subterm_with_head_and_args goes under lambdas
---

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 85c385e..c8710f4 100644
--- 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
 ;;
 
 let get_subterm_with_head_and_args hd_var n_args =
- let rec aux = function
- | V _ | L _ | B | P -> None
+ let rec aux lev = function
+ | V _ | B | P -> None
+ | L t -> aux (lev+1) t
  | A(t1,t2) as t ->
-   if head_of_inert t1 = hd_var && n_args <= 1 + args_no t1
-    then Some t
-    else match aux t2 with
-    | None -> aux t1
+   if head_of_inert t1 = hd_var + lev && n_args <= 1 + args_no t1 (* why `1+' ?*)
+    then Some (lift ~-lev t)
+    else match aux lev t2 with
+    | None -> aux lev t1
     | Some _ as res -> res
- in aux
+ in aux 0
 ;;
 
 (* let rec simple_explode p =