From 765c6b15b76fd407a4d888d3f5e8cc532901045b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Jan 2018 17:47:25 +0100
Subject: [checker] Remove duplicated function

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

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 22353ec168..fb33cd96b7 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -435,12 +435,6 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let eq_recarg r1 r2 = match r1, r2 with
-| Norec, Norec -> true
-| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
-| _ -> false
-
 let eq_wf_paths = Rtree.equal eq_recarg
 
 let inter_recarg r1 r2 = match r1, r2 with
-- 
cgit v1.2.3