diff options
| author | barras | 2006-10-30 10:26:46 +0000 |
|---|---|---|
| committer | barras | 2006-10-30 10:26:46 +0000 |
| commit | 3fd4c212e742169b80ac709a6a7f68a47eff61b1 (patch) | |
| tree | f0863549f56ddb1ae1ecea179ae8e48d794ba1a9 | |
| parent | f97016c08df3536ee51468a8b22a2a022f3f38a1 (diff) | |
LegacyRfield was opening R_scope
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9317 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/LegacyRfield.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v index d285fef30e..b33274af92 100644 --- a/theories/Reals/LegacyRfield.v +++ b/theories/Reals/LegacyRfield.v @@ -11,6 +11,9 @@ Require Export Raxioms. Require Export LegacyField. Import LegacyRing_theory. + +Section LegacyRfield. + Open Scope R_scope. Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false). @@ -30,6 +33,8 @@ Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false). intros; contradiction. Defined. +End LegacyRfield. + Add Legacy Field -R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l +R Rplus Rmult 1%R 0%R Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l with minus := Rminus div := Rdiv. |