From 777f0ace3d2458cbe1840dcf3d8f350452721e84 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Feb 2015 09:30:53 +0100
Subject: Removing dead code.

---
 kernel/inductive.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bb57ad2566..6b4dd536a1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -447,13 +447,6 @@ type subterm_spec =
 
 let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
-let pp_recarg = function
-  | Norec -> Pp.str "Norec"
-  | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i))
-  | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i))
-
-let pp_wf_paths = Rtree.pp_tree pp_recarg
-
 let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
 | Mrec i1, Mrec i2
-- 
cgit v1.2.3