From 72498d6d68ac12ba4db0db7d54f0ac6fdaaf0c61 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 18 Aug 2014 17:13:19 +0200 Subject: Adding a new intro-pattern for "apply in" on the fly. Using syntax "pat/term" for "apply term on current_hyp as pat". --- tactics/inv.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics/inv.mli') diff --git a/tactics/inv.mli b/tactics/inv.mli index 7416d29bb..a71b5eeb3 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -15,14 +15,14 @@ open Tacexpr type inversion_status = Dep of constr option | NoDep val inv_clause : - inversion_kind -> or_and_intro_pattern_expr located option -> Id.t list -> + inversion_kind -> constr or_and_intro_pattern_expr located option -> Id.t list -> quantified_hypothesis -> unit Proofview.tactic -val inv : inversion_kind -> or_and_intro_pattern_expr located option -> +val inv : inversion_kind -> constr or_and_intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic val dinv : inversion_kind -> constr option -> - or_and_intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic + constr or_and_intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic val inv_tac : Id.t -> unit Proofview.tactic val inv_clear_tac : Id.t -> unit Proofview.tactic -- cgit v1.2.3