diff options
| author | Hugo Herbelin | 2020-08-21 20:53:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 11:45:32 +0100 |
| commit | 47c05b2531cb0de6da91968e2d17c68033ae7835 (patch) | |
| tree | 3d85f8af2561029b6b13952c54892b06024d135c /dev/ci | |
| parent | 4775fd7724840205b345420507bdd1c7065059b0 (diff) | |
Fixing a (known) "bugged" part of imitation in unification.
We ensure that when imitation stops to be possible, we postpone an
equation of the type of the subterm (and not of the arbitrary type of
an evar possibly depending on this subterm).
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions