diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/BigQ.v')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index a2bc5e266..50c90757a 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -38,9 +38,8 @@ End BigN_BigZ. Delimit Scope bigQ_scope with bigQ. Module BigQ <: QType <: OrderedTypeFull <: TotalOrder. - Include QMake.Make BigN BigZ BigN_BigZ [scope abstract_scope to bigQ_scope]. - Bind Scope bigQ_scope with t t_. - Include !QProperties <+ HasEqBool2Dec + Include QMake.Make BigN BigZ BigN_BigZ + <+ !QProperties <+ HasEqBool2Dec <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. Ltac order := Private_Tac.order. End BigQ. |