diff options
| author | Hugo Herbelin | 2018-04-26 15:43:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 14:21:10 +0200 |
| commit | cfefed1cb20b6abe33c222df49d346867bafbc7f (patch) | |
| tree | b5d63aca3ec9f29f3e74cc4427575b4b734dbda5 /kernel/modops.ml | |
| parent | 64a8f3cbb2fa278ed9d7bf2e5567d4e2b9bfa9dc (diff) | |
Preparing ability to select "best" unification failure to report among two.
Diffstat (limited to 'kernel/modops.ml')
0 files changed, 0 insertions, 0 deletions