aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Coqlib.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r--lib/Coqlib.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 3fe1ea2e..3b8e5b3b 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -17,6 +17,7 @@
used throughout the development. It complements the Coq standard
library. *)
+Require Export String.
Require Export ZArith.
Require Export Znumtheory.
Require Export List.