diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index fa6007061..66aee0313 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -128,7 +128,9 @@ val no_focused_goal : proof -> bool (*** Tactics ***) -val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof +(* the returned boolean signal whether an unsafe tactic has been + used. In which case it is [false]. *) +val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof*bool val emit_side_effects : Declareops.side_effects -> proof -> proof |