diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
| commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
| tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/funind/invfun.ml | |
| parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) | |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/funind/invfun.ml')
| -rw-r--r-- | contrib/funind/invfun.ml | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 1f711297..2e5616f0 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 @@ -114,7 +105,7 @@ let invfun (hypname:identifier) (fid:identifier) : tactic= let frealargs = (snd (array_chop (List.length princ_info.params) fargs)) in let pat_args = - (List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf] + (List.map (fun e -> ([Rawterm.ArgArg (-1)],e)) (Array.to_list frealargs)) @ [[],appf] in tclTHENSEQ [ |