diff options
| author | Pierre-Marie Pédrot | 2020-07-04 23:58:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-02 18:00:52 +0200 |
| commit | 7b4f197d37a5f1bdf470676f6879c607a45a3477 (patch) | |
| tree | f908ba29b9623835bad806e01e0c6ead7667727d /dev/include_dune | |
| parent | cc51e1fd680c1f1bf47cc8b504196c9f2677fa3b (diff) | |
Use a dedicated type for equality elimination.
In this mess of higher-order callbacks it helps sorting out the invariants
of the structure.
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions