diff options
| author | Hugo Herbelin | 2014-08-02 09:30:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:21 +0200 |
| commit | 0e6facc70506d81e765c5a0be241a77bc7b22b85 (patch) | |
| tree | ba0f92d3bf019d5cbf4c72b2f2b667457052f179 /intf | |
| parent | f9517286637fd0891a3ac1aac041b437e157f756 (diff) | |
Adding a syntax "enough" for the variant of "assert" with the order of
subgoals and the role of the "by tac" clause swapped.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 22ec1b4459..4174de1230 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -117,7 +117,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of - ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option * + bool * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option * intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacGeneralizeDep of 'trm |