diff options
| author | Pierre-Marie Pédrot | 2020-04-30 16:13:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | 86751a2069fd3360742d44dbe66c221894196ad6 (patch) | |
| tree | 3475922a21c4d56d9070f08a0c05d02f9d2cdc95 /plugins/syntax | |
| parent | c459cbd09ec16dd7e6767ac4ffe55e19747f4705 (diff) | |
Wrap ssr tactics into V82.tactic.
Porting them is still to be done, but at least we don't rely on the wrapper
everywhere.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions