diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 15 |
2 files changed, 8 insertions, 9 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 49fc513dd2..b864b18887 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -116,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) = refine to_refine g) ] let find_rectype env sigma c = - let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in + let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in match EConstr.kind sigma t with | Ind ind -> (t, l) | Construct _ -> (t, l) diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 68e1087b74..a1094e39a4 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -18,6 +18,7 @@ open Indfun_common open Indfun open Stdarg open Tacarg +open Extraargs open Tactypes open Pcoq.Prim open Pcoq.Constr @@ -96,14 +97,12 @@ let functional_induction b c x pat = } TACTIC EXTEND newfunind -| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - { - let c = match cl with - | [] -> assert false - | [c] -> c - | c::cl -> EConstr.applist(c,cl) - in - Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl } +| ["functional" "induction" lconstr(c) fun_ind_using(princl) with_names(pat)] -> + { + (Extratactics.onSomeWithHoles + (fun x -> functional_induction true c x pat) princl) + } + END (***** debug only ***) TACTIC EXTEND snewfunind |