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 _ -> problem_fail p "no eta difference found (div subterm of conv?)"\r
+ | V _, V _ -> None\r
| A(t1,t2), A(u1,u2) ->\r
- if not (eta_eq t2 u2) then (k-1)\r
- else aux t1 u1 (k-1)\r
+ (match aux t1 u1 (k-1) with\r
+ | None ->\r
+ if not (eta_eq t2 u2) then Some (k-1)\r
+ else None\r
+ | Some j -> Some j)\r
| _, _ -> assert false\r
- in aux p.div t argsno\r
+ in match aux p.div t argsno with\r
+ | None -> problem_fail p "no eta difference found (div subterm of conv?)"\r
+ | Some j -> j\r
;;\r
\r
let compute_max_lambdas_at hd_var j =\r
let p, v = freshvar p in\r
p, A(t, V (v + k + 1))\r
) (p, V 0) n in\r
- let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
- fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
+ let t = (* apply bound variables V_k..V_0 *)\r
+ fold_nat (fun t m -> A(t, V (k-m+1))) t (k+1) in\r
let t = mk_lams t (k+1) in (* make leading lambdas *)\r
let subst = var, t in\r
let p = subst_in_problem subst p in\r