diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 10:15:28 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 10:15:28 +0200 |
commit | acbc42ad1da48be53456c0d41ec2e60ae2d6e642 (patch) | |
tree | 997d7e949de3541111ec01708be973abb678f24b /kernel/cooking.mli | |
parent | fc4f18c84bfc421dff55c77aa564abc1ea20f528 (diff) | |
parent | 315aa093490d533e3d8db7a24bde78ed812c3b0d (diff) |
Merge PR #7890: Inline a function from Quote used in setoid_ring.
Diffstat (limited to 'kernel/cooking.mli')
0 files changed, 0 insertions, 0 deletions