diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 22:52:48 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 22:52:48 +0200 |
| commit | eb9c9df833ae908a6e0e22260439fc263aed2b6b (patch) | |
| tree | 184d3866966553718c0eeaeb52772f15ea32a2b4 /plugins/setoid_ring/Rings_R.v | |
| parent | 216c6c89d53e58eefff5ac8d47e1c5e04cdbf4b0 (diff) | |
| parent | abd6bbd90753fd98355e551d8dc8ecfd07494639 (diff) | |
Merge PR #7264: [Sphinx] Fix a lot of references and description of options
Diffstat (limited to 'plugins/setoid_ring/Rings_R.v')
0 files changed, 0 insertions, 0 deletions