aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrtacticals.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrtacticals.mli')
-rw-r--r--plugins/ssr/ssrtacticals.mli5
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index c1f65a31e..5913c09d4 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -19,14 +19,13 @@ val tclSEQAT :
Tacmach.tactic
val tclCLAUSES :
- Ltac_plugin.Tacinterp.interp_sign ->
- Proofview.V82.tac ->
+ unit Proofview.tactic ->
(Ssrast.ssrhyps *
((Ssrast.ssrhyp_or_id * string) *
Ssrmatching_plugin.Ssrmatching.cpattern option)
option)
list * Ssrast.ssrclseq ->
- Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+ unit Proofview.tactic
val hinttac :
Tacinterp.interp_sign ->