diff options
| author | Hugo Herbelin | 2017-08-13 20:05:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:04 +0100 |
| commit | d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 (patch) | |
| tree | 4843bf72c79905f811d6f3f5ac4cdd4d81943e65 /interp/notation.ml | |
| parent | 7c10b4020e061fb14e01cb3abc92bb5265aa65b9 (diff) | |
Allows recursive patterns for binders to be associative on the left.
This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.
Example of (artificial) notation that this commit supports:
Notation "! x .. y # A #" :=
(.. (A,(forall x, True)) ..,(forall y, True))
(at level 200, x binder).
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 94ce2a6c8d..31f16e1a90 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -292,7 +292,7 @@ let cases_pattern_key c = match DAst.get c with let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) | NList (_,_,NApp (NRef ref,args),_,_) - | NBinderList (_,_,NApp (NRef ref,args),_) -> + | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | NApp (_,args) -> Oth, Some (List.length args) |