diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:19 +0000 |
| commit | b5011fe9c8b410074f2b1299cf83aabed834601f (patch) | |
| tree | eb433f71ae754c1f2526bb55f7eb83bb81300dd4 /contrib/ring/Ring_abstract.v | |
| parent | 16d5d84c20cc640be08c3f32cc9bde5cbd3f06dd (diff) | |
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring/Ring_abstract.v')
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index bd1fc79b6..f2fe16f3a 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -459,7 +459,7 @@ Save. Hint rew_isacs_aux : core := Extern 10 (eqT A ? ?) Rewrite isacs_aux_ok. -Tactic Definition Solve1 := +Tactic Definition Solve1 v v0 H H0 := Simpl; Elim (varlist_lt v v0); Simpl; Rewrite isacs_aux_ok; [Rewrite H; Simpl; Auto |Simpl in H0; Rewrite H0; Auto ]. @@ -475,7 +475,7 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum) Auto. - Solve1. + Solve1 v v0 H H0. Simpl; Generalize (varlist_eq_prop v v0). Elim (varlist_eq v v0); Simpl. @@ -491,7 +491,7 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum) Rewrite (Th_plus_zero_left T). Reflexivity. - Solve1. + Solve1 v v0 H H0. Induction y; Intros. @@ -509,13 +509,13 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum) Rewrite (Th_plus_zero_left T). Reflexivity. - Solve1. + Solve1 v v0 H H0. - Solve1. + Solve1 v v0 H H0. Save. -Tactic Definition Solve2 := +Tactic Definition Solve2 l v H := Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok; [ Auto | Rewrite H; Auto ]. @@ -529,7 +529,7 @@ Proof. Trivial. Simpl; Intros. - Solve2. + Solve2 l v H. Simpl; Intros. Generalize (varlist_eq_prop l v). @@ -542,7 +542,7 @@ Proof. Rewrite (Th_plus_zero_left T). Reflexivity. - Solve2. + Solve2 l v H. Save. @@ -567,9 +567,9 @@ Proof. Auto. Simpl; Intros. - Solve2. + Solve2 l v H. - Simpl; Intros; Solve2. + Simpl; Intros; Solve2 l v H. Save. |