From 407e154baa44609dea9f6f1ade746e24d60e2513 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 9 Aug 2017 14:00:26 +0200 Subject: Rephrasing ETBinderList with a self-documenting and invariant-carrying argument. --- vernac/metasyntax.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'vernac/metasyntax.ml') 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 -- cgit v1.2.3