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 range i j =\r
+ if j = -1 then [] else i :: range (i+1) (j-1) in\r
let rec aux k divargs conargs =\r
match divargs,conargs with\r
- [],_ -> []\r
+ [],conargs -> range k (List.length conargs)\r
| _::_,[] -> [k]\r
| t1::divargs,t2::conargs ->\r
(if not (eta_eq t1 t2) then [k] else []) @ aux (k+1) divargs conargs\r