diff options
| author | Hugo Herbelin | 2020-08-31 20:19:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-02 23:29:14 +0200 |
| commit | d680b80092861b0c10e220cdf8d91e8ae35c0252 (patch) | |
| tree | 018487d23a2f120374e94b78899525c75872f873 /interp/implicit_quantifiers.ml | |
| parent | e9b64e2f09d2a8dcc2558a9ea34268b4d78fdc66 (diff) | |
Fixes #9403 and #10803 (missing flattening of nested applications in notations).
The bugs involved:
- a notation with a subterm in position of function of an application
- use of this notation in another notation creating a non-flattened application
In particular, this fooled "find_appl_head" (for #10803) and the
translation from GApp to NApp (for #9403).
We fix the translation NApp -> GApp (since glob_constr is supposed to
have its applications flattened).
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions