diff options
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 144b59f4d..9b5015e0c 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -87,7 +87,7 @@ val with_current_proof : (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit val set_interp_tac : - (Tacexpr.raw_tactic_expr -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma) + (Tacexpr.raw_tactic_expr -> unit Proofview.tactic) -> unit (** Sets the section variables assumed by the proof *) |