diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-09 14:00:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:03 +0100 |
| commit | 407e154baa44609dea9f6f1ade746e24d60e2513 (patch) | |
| tree | d29ce22e16bdd2a243f45d16f6a07ec81a299f18 /vernac/metasyntax.ml | |
| parent | 66eae7fa7f8e1f075a8c84afad48af4d35c4bfaf (diff) | |
Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c295434d0..bb4db1322 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -656,8 +656,10 @@ let make_production etyps symbols = let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in expand_list_rule typ tkl x 1 p (aux l') | ETBinder o -> + check_open_binder o sl x; + let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in distribute - [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] (aux l) + [GramConstrNonTerminal (ETBinderList typ, Some x)] (aux l) | _ -> user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.") in let prods = aux symbols in |