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.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.ml')
| -rw-r--r-- | interp/notation.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 948ebe9640..1a361dc1a6 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -391,6 +391,10 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), AppBoundedNotation (List.length args) | NRef ref -> RefKey(canonical_gr ref), NotAppNotation + | NApp (NList (_,_,NApp (NRef ref,args),_,_), args') -> + RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args') + | NApp (NList (_,_,NApp (_,args),_,_), args') -> + Oth, AppBoundedNotation (List.length args + List.length args') | NApp (_,args) -> Oth, AppBoundedNotation (List.length args) | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation | _ -> Oth, NotAppNotation |