aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrfwd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrfwd.mli')
-rw-r--r--plugins/ssr/ssrfwd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 2de10837c5..dc90b159d7 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -31,7 +31,7 @@ val havetac : ist ->
val basecuttac :
string ->
- EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma
+ EConstr.t -> unit Proofview.tactic
val wlogtac :
Ltac_plugin.Tacinterp.interp_sign ->