diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 10:07:35 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 10:07:35 +0100 |
| commit | ddc9728030a98b03447e321d2eb4af0d92add11f (patch) | |
| tree | 6892bdb6f90ff1978824b1d2bc07f534d14d9167 /plugins/ssr/ssripats.mli | |
| parent | 273089065edaf5d926ad820d3bc3c0dacec1b75d (diff) | |
| parent | 0b1032f2acdb6f7d92c84ba3afcbf3818cc107a9 (diff) | |
Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.
Diffstat (limited to 'plugins/ssr/ssripats.mli')
| -rw-r--r-- | plugins/ssr/ssripats.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index b8716c0c4..89cba4be7 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -29,11 +29,11 @@ val tclIPATssr : ssripats -> unit Proofview.tactic [tac E: gens => ipats] where [E] is injected into [ipats] (at the right place) and [gens] are generalized before calling [tac] *) -val ssrmovetac : ssrmovearg -> unit Proofview.tactic +val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrsmovetac : unit Proofview.tactic -val ssrelimtac : ssrmovearg -> unit Proofview.tactic +val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrselimtoptac : unit Proofview.tactic -val ssrcasetac : ssrmovearg -> unit Proofview.tactic +val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrscasetoptac : unit Proofview.tactic (* The implementation of abstract: is half here, for the [[: var ]] |