diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index b5fc9ee66f..6f11e71156 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -30,9 +30,9 @@ val apply_sig_tac : (** [abstract_tactic tac] hides the (partial) proof produced by [tac] under a single proof node. The boolean tells if the default tactic is used. *) -(* spiwack: currently here for compatibility, abstract_operation - is a second projection *) -val abstract_operation : compound_rule -> tactic -> tactic +(* spiwack: currently here for compatibility, the tactic expression + is discarded and we simply return the tactic. *) + val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic val abstract_extended_tactic : |