--- a/src/Tactics.v	Wed Dec 16 17:31:57 2009 -0500
+++ b/src/Tactics.v	Mon Dec 28 12:35:44 2009 -0500
@@ -157,24 +157,25 @@
            | [ H : _ |- _ ] => clear H
          end.
 
-Ltac guess tac H :=
+Ltac guess v H :=
   repeat match type of H with
            | forall x : ?T, _ =>
              match type of T with
                | Prop =>
                  (let H' := fresh "H'" in
                    assert (H' : T); [
-                     solve [ tac ]
+                     solve [ eauto 6 ]
                      | generalize (H H'); clear H H'; intro H ])
                  || fail 1
                | _ =>
-                 let x := fresh "x" in
+                 (generalize (H v); clear H; intro H)
+                 || let x := fresh "x" in
                    evar (x : T);
                    let x' := eval cbv delta [x] in x in
                      clear x; generalize (H x'); clear H; intro H
              end
          end.
 
-Ltac guessKeep tac H :=
+Ltac guessKeep v H :=
   let H' := fresh "H'" in
-    generalize H; intro H'; guess tac H'.
+    generalize H; intro H'; guess v H'.