From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 8 Jul 2016 14:43:57 +0200
Subject: Port to Coq 8.5pl2

Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
---
 lib/Wfsimpl.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'lib/Wfsimpl.v')

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.
 
 
-
-- 
cgit