From 8a3cd2fe699540f1ae5a56917d0f6b951f81d731 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:29:35 +0200
Subject: Remove unused [rec] keywords

---
 checker/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/inductive.ml')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index c4ffc141ff..ae2f7de8ab 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -149,7 +149,7 @@ let remember_subst u subst =
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env =
+let make_subst env =
   let rec make subst = function
     | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

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

(limited to 'checker/inductive.ml')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index ae2f7de8ab..8f23a38afc 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -436,13 +436,6 @@ let eq_recarg r1 r2 = match r1, r2 with
 
 let eq_wf_paths = Rtree.equal 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