aboutsummaryrefslogtreecommitdiffstats
path: root/backend/SelectDiv.vp
diff options
context:
space:
mode:
Diffstat (limited to 'backend/SelectDiv.vp')
-rw-r--r--backend/SelectDiv.vp2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 5cc66322..dc85fb25 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -17,7 +17,7 @@ Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel SelectOp SplitLong SelectLong.
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
(** We try to turn divisions by a constant into a multiplication by
a pseudo-inverse of the divisor. The approach is described in