diff options
| author | Pierre-Marie Pédrot | 2017-07-12 11:44:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-12 11:44:53 +0200 |
| commit | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (patch) | |
| tree | 5beee0d40d95aa08f3f0030cb419c63894679238 /plugins/syntax/string_syntax.ml | |
| parent | 91df402729f70144a4e4d198c4384dc515920e59 (diff) | |
Adding a comment regarding De Bruijn universe indices in the kernel.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions