aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/Maps.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/common/Maps.v')
-rw-r--r--src/common/Maps.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 3236417..b5a2fb2 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -1,4 +1,4 @@
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
From compcert Require Export Maps.
From compcert Require Import Errors.