diff options
| author | Gabriel Scherer | 2015-06-27 22:23:41 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 12:45:41 +0200 |
| commit | 5a212ff444e9e231f5b56629e5cf15087bac69c6 (patch) | |
| tree | 2ad44a284c1e45dbc7a4f29075b94c2a53615a8b /dev/base_include | |
| parent | 56a7d450fb67268d121e69a5e111968d0dfb2a6a (diff) | |
minor: in constrintern.ml:sort_fields, clarify sf
The internal `add_pat` function is replaced by a call to
`CList.extract_first`.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions