From f461e7657cab9917c5b405427ddba3d56f197efb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 8 May 2016 18:59:55 +0200
Subject: Removing dead code and unused opens.

---
 plugins/funind/functional_principles_proofs.ml | 1 -
 plugins/funind/g_indfun.ml4                    | 3 ---
 plugins/funind/recdef.ml                       | 2 +-
 3 files changed, 1 insertion(+), 5 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 02cd819f4a..8395865286 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -5,7 +5,6 @@ open Term
 open Vars
 open Namegen
 open Names
-open Declarations
 open Pp
 open Tacmach
 open Termops
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0ba18f568a..6dfc23511e 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -9,15 +9,12 @@
 open Compat
 open Util
 open Term
-open Vars
-open Names
 open Pp
 open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
 open Constrarg
-open Tacticals
 open Misctypes
 open Pcoq.Prim
 open Pcoq.Constr
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 046c7aa437..e98ac5fb5e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -208,7 +208,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob
 (* Debugging mechanism *)
 let debug_queue = Stack.create ()
 
-let rec print_debug_queue b e = 
+let print_debug_queue b e = 
   if  not (Stack.is_empty debug_queue) 
   then
     begin
-- 
cgit v1.2.3