2 files changed, 0 insertions, 16 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 28a9542167..cd2ea3ef88 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -27,10 +27,6 @@ let array_get_start a =
     (Array.length a - 1)
     (fun i -> a.(i))
 
-let id_of_name = function
-    Name id -> id
-  | _ -> raise Not_found
-
 let locate qid = Nametab.locate qid
 
 let locate_ind ref =
@@ -105,15 +101,6 @@ let const_of_id id =
     CErrors.user_err ~hdr:"IndFun.const_of_id"
       (str "cannot find " ++ Id.print id)
 
-let def_of_const t =
-   match Constr.kind t with
-    Const sp ->
-      (try (match Environ.constant_opt_value_in (Global.env()) sp with
-             | Some c -> c
-	     | _ -> assert false)
-       with Not_found -> assert false)
-    |_ -> assert false
-
 [@@@ocaml.warning "-3"]
 let coq_constant s =
   UnivGen.constr_of_monomorphic_global @@
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 *)