diff options
Diffstat (limited to 'plugins/micromega/RMicromega.v')
| -rw-r--r-- | plugins/micromega/RMicromega.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index d8282a1127..3651b54ed8 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -41,7 +41,7 @@ Proof. exact Rplus_opp_r. Qed. -Open Scope R_scope. +Local Open Scope R_scope. Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt. Proof. |