X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;h=c7b9a3a9998e33b5eeb822c416196373a536ceed;hb=11118ab13d127a135ef7505909fe0f16740b8ea5;hp=45e605b7ee37160d42c606e864273a0971a31f88;hpb=dc6b7a6afe8b1fcf4f5998089ed2ef28f255da0a;p=fireball-separation.git

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 45e605b..c7b9a3a 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -163,9 +163,9 @@ let rec subst top level delift ((flag, var, tm) as sub) =
         assert (match t1' with L _ -> false | _ -> true) ;
         (match flag with
           | `Some b when !b -> b := false
-          | `Some b ->
-            print_string "WARNING! Stepping on a useless argument!";
-            ignore(read_line())
+          | `Some b -> ()
+            (*print_string "WARNING! Stepping on a useless argument!";
+            ignore(read_line())*)
           | `Inherit | `Duplicate -> assert false);
         A(flag, t1', erase t2')
     | `Inherit | `Duplicate ->
@@ -283,10 +283,18 @@ 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 _ -> None
- | A(_,t1,t2), A(_,u1,u2) ->
+ | A(b1,t1,t2), A(b2,u1,u2) ->
     (match aux t1 u1 (k-1) with
     | None ->
-      if not (eta_eq t2 u2) then Some (k-1)
+      if not (eta_eq t2 u2) then begin
+        let is_relevant = function `Some b -> !b | _ -> false in
+        if not (is_relevant b1 || is_relevant b2) then begin
+         print_string "WARNING! Stepping on a useless argument!";
+print_string (string_of_t  t ^ " <==> " ^ string_of_t u);
+         ignore(read_line())
+        end ;
+        Some (k-1)
+       end
       else None
     | Some j -> Some j)
  | _, _ -> assert false