diff options
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 3722d4727d..8cf5b26fb1 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -146,7 +146,8 @@ Definition lt_compat := lt_wd. Definition lt_total := lt_trichotomy. Definition le_lteq := lt_eq_cases. -Module OrderElts <: TotalOrder. +Module Private_OrderTac. +Module Elts <: TotalOrder. Definition t := t. Definition eq := eq. Definition lt := lt. @@ -156,9 +157,10 @@ Module OrderElts <: TotalOrder. Definition lt_compat := lt_compat. Definition lt_total := lt_total. Definition le_lteq := le_lteq. -End OrderElts. -Module OrderTac := !MakeOrderTac OrderElts. -Ltac order := OrderTac.order. +End Elts. +Module Tac := !MakeOrderTac Elts. +End Private_OrderTac. +Ltac order := Private_OrderTac.Tac.order. (** Some direct consequences of [order]. *) |