X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;fp=ocaml%2Fsimple.ml;h=aa91996027a513fc5f8eaface109bdd8d0bf9600;hb=ecf29d252b740979357afcfa26173b09ea4c95f9;hp=9de1f2a7c12444f2b651628d7d499e7e8497871b;hpb=ad332f3befc4922498db7a9ca6dbb7cc67dbf75b;p=fireball-separation.git

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 9de1f2a..aa91996 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -206,12 +206,17 @@ let inert_cut_at n t =
 let find_eta_difference p t argsno =
  let t = inert_cut_at argsno t in
  let rec aux t u k = match t, u with
- | V _, V _ -> problem_fail p "no eta difference found (div subterm of conv?)"
+ | V _, V _ -> None
  | A(t1,t2), A(u1,u2) ->
-    if not (eta_eq t2 u2) then (k-1)
-    else aux t1 u1 (k-1)
+    (match aux t1 u1 (k-1) with
+    | None ->
+      if not (eta_eq t2 u2) then Some (k-1)
+      else None
+    | Some j -> Some j)
  | _, _ -> assert false
- in aux p.div t argsno
+ in match aux p.div t argsno with
+ | None -> problem_fail p "no eta difference found (div subterm of conv?)"
+ | Some j -> j
 ;;
 
 let compute_max_lambdas_at hd_var j =
@@ -269,8 +274,8 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
     let p, v = freshvar p in
     p, A(t, V (v + k + 1))
   ) (p, V 0) n in
- let t = (* apply unused bound variables V_{k-1}..V_1 *)
-  fold_nat (fun t m -> A(t, V (k-m+1))) t k in
+ let t = (* apply bound variables V_k..V_0 *)
+  fold_nat (fun t m -> A(t, V (k-m+1))) t (k+1) in
  let t = mk_lams t (k+1) in (* make leading lambdas *)
  let subst = var, t in
  let p = subst_in_problem subst p in