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/notation_ops.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/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6422e184b5..22531b0016 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -187,7 +187,7 @@ let apply_cases_pattern ?loc (ids_disjpat,id) c = let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_status_fun) e nc = let lt x = DAst.make ?loc x in lt @@ match nc with | NVar id -> GVar id - | NApp (a,args) -> let e = h.no e in GApp (f e a, List.map (f e) args) + | NApp (a,args) -> let e = h.no e in DAst.get (mkGApp (f e a) (List.map (f e) args)) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in |