diff options
| author | coqbot-app[bot] | 2020-09-22 17:42:57 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-22 17:42:57 +0000 |
| commit | 46bc7d034aa57c21825371e99b25c6f86c0812d1 (patch) | |
| tree | 927868586fb64c5a4c6810ea59095e99b9fd979c /interp/notation_ops.ml | |
| parent | c3a73c5e923953efea016a81d380e58b2cccb4f9 (diff) | |
| parent | 899e3cd4bba5c6ba0ec6ec60f20acf4ae507fa27 (diff) | |
Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applications in notations
Reviewed-by: ejgallego
Ack-by: maximedenes
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 |