Reorder the steps of the easy tactic. (Fix for bug #2630)

Due to the way it was laid out, the tactic could prove neither
  (Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True)
yet it could prove
  (Zle x x /\ True) and (P /\ Q |- P).

1 files changed, 8 insertions, 6 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9e828e6ea..a7d3f8062 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -180,12 +180,14 @@ Ltac easy :=
     | H : _ |- _ => solve [inversion H]
     | _ => idtac
     end in
-  let rec do_atom :=
-    solve [reflexivity | symmetry; trivial] ||
-    contradiction ||
-    (split; do_atom)
-  with do_ccl := trivial with eq_true; repeat do_intro; do_atom in
-  (use_hyps; do_ccl) || fail "Cannot solve this goal".
+  let do_atom :=
+    solve [ trivial with eq_true | reflexivity | symmetry; trivial | contradiction ] in
+  let rec do_ccl :=
+    try do_atom;
+    repeat (do_intro; try do_atom);
+    solve [ split; do_ccl ] in
+  solve [ do_atom | use_hyps; do_ccl ] ||
+  fail "Cannot solve this goal".
 
 Tactic Notation "now" tactic(t) := t; easy.