diff options
| author | Pierre-Marie Pédrot | 2014-06-10 20:04:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-10 20:04:52 +0200 |
| commit | 024ad666b1ccda47b9c23d7d5bf33a84b3218618 (patch) | |
| tree | 4bad9b8b92562986f09b168ecbc3882536c7d082 /dev/include | |
| parent | 6ac16429294ff3a755c618ece3ba5e22d59e27f9 (diff) | |
Specialize the type of [Univ.compare_neq] so that it is clear it is only used
to recover the trace of a universe inconsistency. Changed its name too btw.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions