diff options
| author | coqbot-app[bot] | 2020-11-18 13:00:03 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-18 13:00:03 +0000 |
| commit | 4a56d4d90294d3f6128d68d7d1d11e3e27ae8b9a (patch) | |
| tree | 96fbb1236ebb85e3ec1be2f49e0a277e793ce5b4 /interp/notation_ops.ml | |
| parent | 73a068c60fcb757d3a07602259196fcd73485c11 (diff) | |
| parent | 18269746e59a5f7a698a68d31635e2b81facf2ab (diff) | |
Merge PR #12765: In recursive notations, accept partial application over the recursive pattern
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: jfehrle
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 2e3fa0aa0e..7cb3ca25ee 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -275,6 +275,12 @@ type found_variables = { let add_id r id = r := { !r with vars = id :: (!r).vars } let add_name r = function Anonymous -> () | Name id -> add_id r id +let mkNApp1 (g,a) = + match g with + (* Ensure flattening of nested applicative nodes *) + | NApp (g,args') -> NApp (g,args'@[a]) + | _ -> NApp (g,[a]) + let is_gvar id c = match DAst.get c with | GVar id' -> Id.equal id id' | _ -> false @@ -443,7 +449,10 @@ let notation_constr_and_vars_of_glob_constr recvars a = aux' c and aux' x = DAst.with_val (function | GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id - | GApp (g,args) -> NApp (aux g, List.map aux args) + | GApp (g,[]) -> NApp (aux g,[]) (* Encoding @foo *) + | GApp (g,args) -> + (* Treat applicative notes as binary nodes *) + let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a) | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c) |