1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Intv.v b/lib/Intv.v
index 57d946e3..a11e619b 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -18,7 +18,7 @@
 Require Import Coqlib.
 Require Import Zwf.
 Require Coq.Program.Wf.
-Require Recdef.
+Require Import Recdef.
 
 Definition interv : Type := (Z * Z)%type.