diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /theories/Init/Tactics.v | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
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 9e828e6e..a7d3f806 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. |