diff options
| author | Emilio Jesus Gallego Arias | 2019-07-19 03:41:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-07 19:44:29 +0200 |
| commit | e3e2bec0f31390fe797d65961a14f7cd78bc4109 (patch) | |
| tree | fe5fbc579fedf22298ed72222976c78993afed38 /plugins/funind/indfun_common.ml | |
| parent | 0d61500c7137f93942a63a356226276c26edfd99 (diff) | |
[funind] Port indfun to the new tactic engine.
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 52a29fb559..8471dfd05a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -92,13 +92,6 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l -let const_of_id id = - let princ_ref = qualid_of_ident id in - try Constrintern.locate_reference princ_ref - with Not_found -> - CErrors.user_err ~hdr:"IndFun.const_of_id" - (str "cannot find " ++ Id.print id) - [@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_monomorphic_global @@ |