diff options
| author | Pierre-Marie Pédrot | 2020-08-29 18:51:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-02 19:06:33 +0200 |
| commit | 6060c63e75e12b3671019dfaabfb118b69fd2005 (patch) | |
| tree | d1ddc9aef157ee7a48c0b88945f70080750234c8 /tactics | |
| parent | 007f760ddc7ad0960e91307d02bfc7fef42dc46b (diff) | |
Make the Elim.branch_args type opaque.
Diffstat (limited to 'tactics')
| -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) -> |