Require Znumtheory before using it

For https://github.com/rocq-prover/stdlib/pull/136

Thank you!

added 1 commit

• 0c99696a - Update definitions.v

Compare with previous version

Shouldn't it be Require Import to actually get those names in scope?

Cc @msammler

Znumetheory was not Exported from stdlib, so Import shouldn't be required. It'd be fine to add it, of course. Znumtheory.Zmod_div_mod is referenced with a qualified name below.

Here's how I tested

$ git -C _build_ci/stdlib log --oneline -1
65ff9c5 (HEAD) split Zdivisibility from Znumtheory, deprecate most of Znumtheory
$ git -C _build_ci/stdpp/ diff
diff --git a/stdpp_bitvector/definitions.v b/stdpp_bitvector/definitions.v
index 36a1b73..422d77e 100644
--- a/stdpp_bitvector/definitions.v
+++ b/stdpp_bitvector/definitions.v
@@ -1,4 +1,5 @@
 (** This file is maintained by Michael Sammler. *)
+From Stdlib Require Znumtheory.
 From stdpp Require Export numbers.
 From stdpp Require Import countable finite.
 From stdpp Require Import options.
$ # make ci-iris
$ tail -1 iris.log
iris exit code: 0

Okay, fair -- makes sense. Let's just land this, we can always clean up more later.

mentioned in commit fd17255c

merged