aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Rational/BigQ
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Rational/BigQ')
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 0973b7d8d..59bd57084 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -36,7 +36,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
(** Specification with respect to [QArith] *)
- Open Local Scope Q_scope.
+ Local Open Scope Q_scope.
Definition of_Z x: t := Qz (Z.of_Z x).