diff options
| author | Enrico Tassi | 2021-01-06 17:31:33 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | 0a531fae53c31ef76ff25fbfd3ceb8b5b33aa264 (patch) | |
| tree | d528c369ca7797a746666977258482f7e32c7b5f /plugins/syntax/string_notation.mli | |
| parent | 2caae4d530ba97ced98711986dc504f9becdab81 (diff) | |
[coqargs] use standard option injection for -type-in-type
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions