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 2f3378a88..84b184713 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -21,14 +21,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 ->