diff options
| author | Pierre-Marie Pédrot | 2020-05-08 16:29:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | 3af3409a8ec23deb3e0d32f00a31363a36f6209b (patch) | |
| tree | 7bcc87fd19a80424dfad1094b935ced9a7079811 /dev/base_include | |
| parent | be56f39ecfc0726772cc6930dbc7657348f008e1 (diff) | |
Generalize the interpretation of syntactic notation as reference to their head.
This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.
We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions