aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrbwd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrbwd.mli')
-rw-r--r--plugins/ssr/ssrbwd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index 6243e5e68..694ecfa37 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -13,4 +13,4 @@ open Proofview
val apply_top_tac : unit tactic
-val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic
+val inner_ssrapplytac : ssrterm list -> ssrterm ssragens -> ist -> unit tactic