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.ml | 13 -------------
 1 file changed, 13 deletions(-)

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

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 @@
-- 
cgit v1.2.3