diff options
author | 2015-02-25 15:30:16 +0100 | |
---|---|---|
committer | 2015-02-25 15:39:18 +0100 | |
commit | 09fcaf0c38580cc1cb279974517e2ea77c982da3 (patch) | |
tree | 3d6e4b6109ff802cc73b324dcf5d4e959b94ae17 /theories/Init/Tactics.v | |
parent | d1cbd0b21dd73e2b4af3ced394b51877afde40b8 (diff) |
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).
Diffstat (limited to 'theories/Init/Tactics.v')
-rw-r--r-- | theories/Init/Tactics.v | 14 |
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. |