diff options
| author | Emilio Jesus Gallego Arias | 2018-08-06 18:45:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-08-06 18:45:53 +0200 |
| commit | 18b662aa306c58d46292bdf79a2929c91d7d96fd (patch) | |
| tree | adb9807d935db0fd7c287ce765694512549baf93 /kernel/constr.ml | |
| parent | 4c639d8e97a35c87f24287ab1cd6825adc26fa08 (diff) | |
| parent | 53117df11ef6a8f76a8bce8c62399f4baaa9f9f1 (diff) | |
Merge PR #8189: Some trivial fixes to the custom entry documentation.
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions