diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 6f11e71156..bc47a73c9f 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -33,10 +33,9 @@ val apply_sig_tac : (* 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 : - ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic +val abstract_tactic : tactic -> tactic +val abstract_tactic_expr : tactic -> tactic +val abstract_extended_tactic : tactic -> tactic val refiner : rule -> tactic |