diff --git a/DiscreteProb.v b/DiscreteProb.v
index 10e2ed3..9b61a22 100644
--- a/DiscreteProb.v
+++ b/DiscreteProb.v
@@ -1,4 +1,4 @@
-Require Import VectorStates Measurement.
+Require Import Bits VectorStates Measurement.
 
 (** This file describes some theory of discrete probability distributions.
   Its main feature is 'apply_u', a function to describe the output distribution 
diff --git a/coq-quantumlib.opam b/coq-quantumlib.opam
index 23f69e4..2dfd645 100644
--- a/coq-quantumlib.opam
+++ b/coq-quantumlib.opam
@@ -14,7 +14,7 @@ doc: "https://inqwire.github.io/QuantumLib/toc.html"
 bug-reports: "https://github.com/inQWIRE/QuantumLib/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq" {>= "8.16" < "8.20"}
+  "coq" {>= "8.12"}
   "odoc" {with-doc}
 ]
 build: [
@@ -31,4 +31,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/inQWIRE/QuantumLib.git"
\ No newline at end of file
+dev-repo: "git+https://github.com/inQWIRE/QuantumLib.git"