diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/BigQ.v')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index c7c7735c0..8323d7884 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -19,9 +19,10 @@ Require Import QbiMake. (* We choose for Q the implemention with multiple representation of 0: 0, 1/0, 2/0 etc *) -Module BigQ := Q0. -Definition bigQ := BigQ.t. +Module BigQ <: QSig.QType := Q0. + +Notation bigQ := BigQ.t. Delimit Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with bigQ. |