aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Wfsimpl.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Wfsimpl.v')
-rw-r--r--lib/Wfsimpl.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v
index 4f80822e..a1e4b4ff 100644
--- a/lib/Wfsimpl.v
+++ b/lib/Wfsimpl.v
@@ -18,7 +18,7 @@
to be defined have non-dependent types, and function extensionality is assumed. *)
Require Import Axioms.
-Require Import Wf.
+Require Import Init.Wf.
Require Import Wf_nat.
Set Implicit Arguments.
@@ -65,4 +65,3 @@ Qed.
End FIXM.
-