diff options
| author | Pierre-Marie Pédrot | 2020-06-08 15:17:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | 21b4e41544f03de18d9f5b1bdb93a26b36a97999 (patch) | |
| tree | 85e1848df45b189ad40693ebe2b651eae9ba2c1f /doc/plugin_tutorial/tuto2/_CoqProject | |
| parent | 2a24a665ca63d82ce2576e75636ab6fdbcad9b36 (diff) | |
Opacify the type of hint metadata.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/_CoqProject')
0 files changed, 0 insertions, 0 deletions