summaryrefslogtreecommitdiff
path: root/theories/Vectors/Vector.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Vectors/Vector.v')
-rw-r--r--theories/Vectors/Vector.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v
index f3e5e338..672858fa 100644
--- a/theories/Vectors/Vector.v
+++ b/theories/Vectors/Vector.v
@@ -18,5 +18,7 @@ Based on contents from Util/VecUtil of the CoLoR contribution *)
Require Fin.
Require VectorDef.
Require VectorSpec.
+Require VectorEq.
Include VectorDef.
Include VectorSpec.
+Include VectorEq. \ No newline at end of file