diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-12 22:25:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:45 +0200 |
| commit | bde36d4b00185065628324d8ca71994f84eae244 (patch) | |
| tree | c4d7bba0352ee72fa31712e02882c7066a6e1ba1 /tactics/tactics.mli | |
| parent | c4d1e3113f77af2e5474fe5676c272050dd445e5 (diff) | |
In the short term, stronger invariant on the syntax of TacAssert, what
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 4c4a96ec0..0919fb28e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -365,7 +365,7 @@ val pose_proof : Name.t -> constr -> (** Common entry point for user-level "assert", "enough" and "pose proof" *) -val forward : bool -> unit Proofview.tactic option -> +val forward : bool -> unit Proofview.tactic option option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactic cut, actually a modus ponens rule *) |