diff options
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 @@ |