diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:32:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:32:55 +0000 |
| commit | 752a947780c13c7afd8ce0624a049e61985e239c (patch) | |
| tree | b088cc9c27771d120c6af6a1edbdaf869821ee6a /contrib/ring | |
| parent | 055466665e4c36b6cce376a27d8685a7a4f0846d (diff) | |
Syntaxe des tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@752 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/ArithRing.v | 3 | ||||
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 14 |
2 files changed, 7 insertions, 10 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v index 5a0842e4b..5f3ff2937 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/ArithRing.v @@ -38,5 +38,4 @@ Goal (n:nat)(S n)=(plus (S O) n). Intro; Reflexivity. Save S_to_plus_one. -Tactic Definition NatRing := - [<:tactic:<(Repeat Rewrite S_to_plus_one); Ring>>]. +Tactic Definition NatRing := '(Repeat Rewrite S_to_plus_one); Ring. diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 3fd77bc5f..6bb1f5aa9 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -443,11 +443,10 @@ Save. Hint rew_isacs_aux : core := Extern 10 (eqT A ? ?) Rewrite isacs_aux_ok. -Tactic Definition Solve1 := [<:tactic:< - Simpl; Elim (varlist_lt v v0); Simpl; Rewrite isacs_aux_ok; - [ Rewrite H; Simpl; Auto - | Simpl in H0; Rewrite H0; Auto ] ->>]. +Tactic Definition Solve1 := + Simpl; Elim (varlist_lt v v0); Simpl; Rewrite isacs_aux_ok; + [Rewrite H; Simpl; Auto + |Simpl in H0; Rewrite H0; Auto ]. Lemma signed_sum_merge_ok : (x,y:signed_sum) (interp_sacs (signed_sum_merge x y)) @@ -500,11 +499,10 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum) Save. -Tactic Definition Solve2 := [<:tactic:< +Tactic Definition Solve2 := Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok; [ Auto - | Rewrite H; Auto ] ->>]. + | Rewrite H; Auto ]. Lemma plus_varlist_insert_ok : (l:varlist)(s:signed_sum) (interp_sacs (plus_varlist_insert l s)) |