diff options
| author | Théo Zimmermann | 2020-11-27 16:22:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-27 16:22:41 +0100 |
| commit | 058ac643c5e93da2472e3a0a717b864f49f90b3b (patch) | |
| tree | 12af50d60c3956ef06375eafa26cda87779e8df8 /plugins/syntax/string_notation.ml | |
| parent | c294664df8e9190a2fbb6153c70c208f58c7db70 (diff) | |
Revert "Remove deprecated tactic cutrewrite."
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions