diff options
| author | Pierre-Marie Pédrot | 2020-07-02 15:38:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | e52a8a898352f55fb544e2b563c81fd1247c8130 (patch) | |
| tree | 4e07d596700b953d64acebc9a00e917620cdc66c /plugins/syntax/string_notation.ml | |
| parent | 85e56b4c25071f048624ffbe7f7891f6f1534127 (diff) | |
Perfom an goal enter in the relevant class tactics instead of outside.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions