From f5837771bf8ac3d22b285129da8f0bf65915098c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 27 Feb 2015 09:42:10 +0100
Subject: [PATCH] move wf_nat_ind to a common place

---
 iris_ht_rules.v | 2 --
 iris_meta.v     | 2 --
 iris_plog.v     | 3 +++
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 203e9d70c..7bf2468e8 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -56,8 +56,6 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         rewrite EQv; reflexivity.
     Qed.
 
-    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
     Lemma htBind P Q R K e safe m :
       ht safe m P e Q ∧ all (plugV safe m Q R K) ⊑ ht safe m P (K [[ e ]]) R.
     Proof.
diff --git a/iris_meta.v b/iris_meta.v
index 5f65742ad..d4382e3c7 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -200,8 +200,6 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
   Set Bullet Behavior "None".	(* PDS: Ridiculous. *)
   Section RobustSafety.
 
-    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
     Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res) (w : Wld) (σ : state).
 
     Program Definition restrictV (Q : expr -n> Props) : vPred :=
diff --git a/iris_plog.v b/iris_plog.v
index 3df7d55d8..7e8b99b43 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -442,6 +442,9 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
     Definition ht safe m P e Q := □(P → wp safe m e Q).
 
+    (* People will need that *)
+    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
+
   End HoareTriples.
 
 End IRIS_PLOG.
-- 
GitLab