From 3c940f8e88e8d57681431c483e6d3e41114c8cc8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 7 Nov 2018 11:53:16 +0000
Subject: [Funind plugin] Remove some dead code

---
 plugins/funind/indfun_common.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'plugins/funind/indfun_common.mli')

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1b4c1248a5..0c8f40c5cf 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -18,8 +18,6 @@ val get_name : Id.t list -> ?default:string -> Name.t -> Name.t
 
 val array_get_start : 'a array -> 'a array
 
-val id_of_name : Name.t -> Id.t
-
 val locate_ind : Libnames.qualid -> inductive
 val locate_constant : Libnames.qualid -> Constant.t
 val locate_with_msg :
@@ -38,7 +36,6 @@ val chop_rlambda_n : int -> Glob_term.glob_constr ->
 val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
 
-val def_of_const : Constr.t -> Constr.t
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
-- 
cgit v1.2.3