diff options
| author | Pierre-Marie Pédrot | 2018-11-12 16:52:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-12 16:52:36 +0100 |
| commit | 040fdec17f7e70fdbef7d400be2dc0e1607a10fa (patch) | |
| tree | 0616768175db18596abbcad32fa1f48f70aae356 /plugins/funind/indfun_common.ml | |
| parent | 78ab6a5263d3d0dd4da300fcfb87c5e896acc153 (diff) | |
| parent | 3c940f8e88e8d57681431c483e6d3e41114c8cc8 (diff) | |
Merge PR #8938: [Plugins] Remove some dead code
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 13 |
1 files changed, 0 insertions, 13 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 @@ |