diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/BinInt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index ad1aefaf13..3a5eb8855e 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -207,7 +207,7 @@ Qed. to prove specifications of operations, but will also be provided later by the generic functor of properties. *) -Module Import BootStrap. +Module Import Private_BootStrap. (** * Properties of addition *) @@ -374,7 +374,7 @@ Proof. rewrite !(mul_comm _ p). apply mul_add_distr_l. Qed. -End BootStrap. +End Private_BootStrap. (** * Proofs of specifications *) |