Ltac2: Avoid generating useless letin when interning { foo with ... }
#2194
| Job | Run time |
|---|---|
| 1h 6m 47s | |
| 1h 6m 47s |
{ foo with ... }
#2194
| Job | Run time |
|---|---|
| 1h 6m 47s | |
| 1h 6m 47s |