diff options
| author | Pierre-Marie Pédrot | 2020-04-30 17:35:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | fcef4f7d643d40cb652580e507d7bda914e8b9f2 (patch) | |
| tree | 4702f08ea499ea1b00ad699ed4942dc880b53ae3 /plugins/ssr/ssrequality.mli | |
| parent | 86751a2069fd3360742d44dbe66c221894196ad6 (diff) | |
Further port SSReflect tactics to the new engine.
Diffstat (limited to 'plugins/ssr/ssrequality.mli')
| -rw-r--r-- | plugins/ssr/ssrequality.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index fc2b75b396..1c3b1bb018 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -26,7 +26,7 @@ val mkclr : ssrclear -> ssrdocc val nodocc : ssrdocc val noclr : ssrdocc -val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic +val simpltac : Ssrast.ssrsimpl -> unit Proofview.tactic val newssrcongrtac : int * Ssrast.ssrterm -> @@ -61,7 +61,7 @@ val ssrrewritetac : Ltac_plugin.Tacinterp.interp_sign -> ssrrwarg list -> unit Proofview.tactic -val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic +val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> unit Proofview.tactic val unlocktac : Ltac_plugin.Tacinterp.interp_sign -> |