diff options
| -rw-r--r-- | tactics/elim.mli | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/tactics/elim.mli b/tactics/elim.mli index 921a942e72..d470309b4a 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -14,13 +14,7 @@ open Tactypes (** Eliminations tactics. *) -type branch_args = private { - ity : Constr.pinductive; (** the type we were eliminating on *) - branchnum : int; (** the branch number *) - nassums : int; (** number of assumptions/letin to be introduced *) - branchsign : bool list; (** the signature of the branch. - true=assumption, false=let-in *) - branchnames : intro_patterns} +type branch_args val case_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> |