diff options
| author | Enrico Tassi | 2019-09-02 15:53:41 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-09-02 15:53:41 +0200 |
| commit | 671bc2bba6576434bee3be5e0b45d4f1515c7443 (patch) | |
| tree | ad0584aedaeb88c439f3d55d857c666f1e0526ec /doc/plugin_tutorial | |
| parent | 61750abbc38dee8f9299b309979e0382d48ac323 (diff) | |
| parent | cff295c4bbc796c4d838842795c324601a2a037c (diff) | |
Merge PR #10719: Make SSR congr tactic work on arrows in Type.
Reviewed-by: gares
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions