diff options
| author | Pierre-Marie Pédrot | 2020-08-29 19:00:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-02 19:06:33 +0200 |
| commit | 1ab01e54cb0f9d48c185e44fbb2191315f97822a (patch) | |
| tree | 1625c70e8d607d88b8bb46729b23e6d3699a8359 /dev/ci | |
| parent | 6060c63e75e12b3671019dfaabfb118b69fd2005 (diff) | |
Factorize the only uses of internal API in Elim for Inv.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions