diff options
Diffstat (limited to 'contrib/funind/invfun.ml')
| -rw-r--r-- | contrib/funind/invfun.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 1f711297aa..85a60bd1c0 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -88,18 +88,9 @@ let gen_fargs fargs : tactic = g -let invfun (hypname:identifier) (fid:identifier) : tactic= +let invfun (hypname:identifier) fname princ : tactic= fun g -> let nprod_goal = nb_prod (pf_concl g) in - let f_ind_id = - ( - Indrec.make_elimination_ident - fid - (Tacticals.elimination_sort_of_goal g) - ) - in - let fname = const_of_id fid in - let princ = const_of_id f_ind_id in let princ_info = let princ_type = (try (match (Global.lookup_constant princ) with |