6 files changed, 7 insertions, 7 deletions
diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc
index 2c2ec8af87..0fb556aa66 100644
--- a/contrib/extraction/test/custom/Adalloc
+++ b/contrib/extraction/test/custom/Adalloc
@@ -1,2 +1,2 @@
-Require Addr.
+Require Import Addr.
 Extraction NoInline ad_double ad_double_plus_un.
diff --git a/contrib/extraction/test/custom/Lsort b/contrib/extraction/test/custom/Lsort
index 41c9db2868..6a1856832d 100644
--- a/contrib/extraction/test/custom/Lsort
+++ b/contrib/extraction/test/custom/Lsort
@@ -1,2 +1,2 @@
-Require Addr. 
+Require Import Addr. 
 Extraction NoInline ad_double ad_double_plus_un.
diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map
index 7f17c34aa2..3e464e3918 100644
--- a/contrib/extraction/test/custom/Map
+++ b/contrib/extraction/test/custom/Map
@@ -1,3 +1,3 @@
-Require Addr.
+Require Import Addr.
 Extraction NoInline ad_double ad_double_plus_un.
 
diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard
index 78c382267b..ca555aa32e 100644
--- a/contrib/extraction/test/custom/Mapcard
+++ b/contrib/extraction/test/custom/Mapcard
@@ -1,4 +1,4 @@
-Require Plus.
+Require Import Plus.
 Extraction NoInline plus_is_one.
-Require Addr.
+Require Import Addr.
 Extraction NoInline ad_double ad_double_plus_un.
diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter
index 41c9db2868..6a1856832d 100644
--- a/contrib/extraction/test/custom/Mapiter
+++ b/contrib/extraction/test/custom/Mapiter
@@ -1,2 +1,2 @@
-Require Addr. 
+Require Import Addr. 
 Extraction NoInline ad_double ad_double_plus_un.
diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v
index ed8dc1084b..45d0a2243d 100644
--- a/contrib/extraction/test/custom/Reals.v
+++ b/contrib/extraction/test/custom/Reals.v
@@ -1,4 +1,4 @@
-Require Reals. 
+Require Import Reals. 
 Extract Inlined Constant R => float.
 Extract Inlined Constant R0 => "0.0".
 Extract Inlined Constant R1 => "1.0".