From e37fe58c2cb0c79e1ffe366464eb9e4123a6caf5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 27 Feb 2015 10:05:10 +0100
Subject: [PATCH] remove duplicate definition

---
 iris_plog.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/iris_plog.v b/iris_plog.v
index 6cac9c751..553ba9c5f 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -471,9 +471,6 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
   End HoareTriples.
 
-  (* Simple things, needed elsewhere. *)
-  Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
 End IRIS_PLOG.
 
 Module IrisPlog (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_PLOG RL C R WP CORE.
-- 
GitLab