diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 1d63fe01a9..e688204a44 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -80,7 +80,7 @@ END let pr_intro_as_pat prc _ _ pat = match pat with | Some pat -> - spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat + spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat | None -> mt () let out_disjunctive = function diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index f88a72ff51..34985f2c48 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 -> - or_and_intro_pattern_expr Loc.located option -> + Term.constr or_and_intro_pattern_expr Loc.located option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma |