- (the first argument is 0)\r
- precondition: p.div and t have n+1 arguments\r
- *)\r
-let find_eta_difference p t argsno =\r
- let t = inert_cut_at argsno t in\r
- let rec aux t u k = match t, u with\r
- | V _, V _ -> []\r
- | A(t1,t2), A(u1,u2) ->\r
- print_endline (string_of_t t2 ^ " vs " ^ string_of_t u2);\r
- if not (eta_eq t2 u2) then (k-1)::aux t1 u1 (k-1)\r
- else aux t1 u1 (k-1)\r
- | _, _ -> assert false\r
- in aux p.div t argsno\r
+ (the first argument is 0) *)\r
+let find_eta_difference p t =\r
+ let divargs = args_of_inert p.div in\r
+ let conargs = args_of_inert t in\r
+ let rec aux k divargs conargs =\r
+ match divargs,conargs with\r
+ [],_ -> []\r
+ | _::_,[] -> [k]\r
+ | t1::divargs,t2::conargs ->\r
+ (if not (eta_eq t1 t2) then [k] else []) @ aux (k+1) divargs conargs\r
+ in\r
+ aux 0 divargs conargs\r