diff options
| author | Enrico Tassi | 2018-09-05 09:55:05 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-07 12:23:06 +0100 |
| commit | df4deb91f818662d4981aec504b3f5bc9625af84 (patch) | |
| tree | 934d4a7516083cdff384645de7e4c5937a325261 /dev | |
| parent | a690e729739635200a8d1fc93ede965cb7e9092b (diff) | |
[doc] adapt comments in plugins/ssr/*.v to coqdoc style
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions