aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/tacexpr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/tacexpr.mli')
-rw-r--r--intf/tacexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 22ec1b445..4174de123 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