diff options
| author | delahaye | 2000-11-28 14:08:18 +0000 |
|---|---|---|
| committer | delahaye | 2000-11-28 14:08:18 +0000 |
| commit | 4800380437b6b133c7a9346aafa9c4e2b76527d7 (patch) | |
| tree | 447b2dfbd93d1e12dc7dcf47f5fd8f105d8d09a1 /contrib/ring | |
| parent | 4c36f26e02e8c1df3f0851250526d89fd81d8448 (diff) | |
Elimination du '
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 55f3e9bf0c..34cb485fd6 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -8,7 +8,7 @@ Implicit Arguments On. Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m. Proof. - Induction n; Induction m; Simpl; Try '(Reflexivity Orelse Contradiction). + Induction n; Induction m; Simpl; Try (Reflexivity Orelse Contradiction). Intros; Rewrite (H i0); Trivial. Intros; Rewrite (H i0); Trivial. Save. @@ -845,7 +845,7 @@ Implicit Arguments Off. Lemma spolynomial_of_ok : (p:polynomial) (interp_p p)==(interp_sp Aplus Amult Azero vm (spolynomial_of p)). -Induction p; Reflexivity Orelse '(Simpl; Intros). +Induction p; Reflexivity Orelse (Simpl; Intros). Rewrite H; Rewrite H0; Reflexivity. Rewrite H; Rewrite H0; Reflexivity. Rewrite H. @@ -857,7 +857,7 @@ Save. Theorem polynomial_normalize_ok : (p:polynomial) (polynomial_normalize p) ==(spolynomial_normalize Aplus Amult Aone (spolynomial_of p)). -Induction p; Reflexivity Orelse '(Simpl; Intros). +Induction p; Reflexivity Orelse (Simpl; Intros). Rewrite H; Rewrite H0; Reflexivity. Rewrite H; Rewrite H0; Reflexivity. Rewrite H; Simpl. |