diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 5 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e688204a44..bbb8a96c54 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -78,10 +78,13 @@ END let pr_intro_as_pat prc _ _ pat = + failwith "todo" +(* match pat with | Some pat -> - spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat + spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat | None -> mt () +*) let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 34985f2c48..e720691406 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -10,7 +10,7 @@ val functional_induction : bool -> Term.constr -> (Term.constr * Term.constr bindings) option -> - Term.constr or_and_intro_pattern_expr Loc.located option -> + Tacexpr.or_and_intro_pattern option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma |