Removed an extra \tacindex occurrence for the tactic discriminate.

Added a tactic "now" which is nonrecursive but generalizes "trivial".


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9884 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index f45b541bc..6c5c0e011 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -126,3 +126,12 @@ bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).
 
 Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) :=
 bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
+
+(** A tactic simpler than auto that is useful for ending proofs "in one step" *)
+Tactic Notation "now" tactic(t) :=
+t;
+match goal with
+| H : _ |- _ => solve [inversion H]
+| _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
+| _ => fail 1 "Cannot solve this goal"
+end.