diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/QMake.v')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 2 |
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). |