diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index a6471be549..9fd50cf0c2 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -81,11 +81,6 @@ val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic val intros : unit Proofview.tactic -(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in - the conclusion of goal [g], up to head-reduction if [b] is [true] *) -val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> Proofview.Goal.t -> int - val intros_until : quantified_hypothesis -> unit Proofview.tactic val intros_clearing : bool list -> unit Proofview.tactic |