diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
| commit | ffb64d16132dd80f72ecb619ef87e3eee1fa8bda (patch) | |
| tree | 5368562b42af1aeef7e19b4bd897c9fc5655769b /test-suite/success/ltac.v | |
| parent | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (diff) | |
Kills the useless tactic annotations "in |- *"
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/ltac.v')
| -rw-r--r-- | test-suite/success/ltac.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 0c8a18167..1edddcfd7 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -2,7 +2,7 @@ (* Submitted by Pierre Crégut *) (* Checks substitution of x *) -Ltac f x := unfold x in |- *; idtac. +Ltac f x := unfold x; idtac. Lemma lem1 : 0 + 0 = 0. f plus. @@ -86,7 +86,7 @@ assert t. exact H. intro H1. apply H. -symmetry in |- *. +symmetry . assumption. Qed. @@ -105,7 +105,7 @@ sym'. exact H. intro H1. apply H. -symmetry in |- *. +symmetry . assumption. Qed. @@ -193,7 +193,7 @@ Abort. (* Used to fail in V8.1 *) Tactic Notation "test" constr(t) integer(n) := - set (k := t) in |- * at n. + set (k := t) at n. Goal forall x : nat, x = 1 -> x + x + x = 3. intros x H. |