diff options
| author | Pierre-Marie Pédrot | 2020-02-03 15:20:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-03 15:29:31 +0100 |
| commit | b9739e398e256fe94f1f52de5868190ec1887ade (patch) | |
| tree | 583c4e7aed52e14fc61f9537c2cf75cc43181778 /kernel/declareops.ml | |
| parent | db2289c50c358ac5bf7c2d2be7b9d255b20173ef (diff) | |
Do not return a full term in Evarsolve alias expansion.
The only user is merely observing whether this can be an rel / var alias.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions