diff options
| author | Hugo Herbelin | 2020-07-28 23:47:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-18 11:28:45 +0100 |
| commit | ca0e42c0ff9e5cebb734bcb59065a4f55ae4aa4e (patch) | |
| tree | 9da6b68e6bd56ced9247ba2135385be8dba86679 /interp/notation.ml | |
| parent | 396de348a4daa2ae752bed8c75a9ecacb4dcd579 (diff) | |
In recursive notations, accept partial application over the recursive pattern.
This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
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 |