diff options
| -rw-r--r-- | test-suite/bugs/closed/5470.v | 3 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 10 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5470.v b/test-suite/bugs/closed/5470.v new file mode 100644 index 0000000000..5b3984b6df --- /dev/null +++ b/test-suite/bugs/closed/5470.v @@ -0,0 +1,3 @@ +(* This used to raise an anomaly *) + +Fail Reserved Notation "x +++ y" (at level 70, x binder). diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e5f8191409..349c05a38d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -809,6 +809,15 @@ let check_useless_entry_types recvars mainvars etyps = (pr_id x ++ str " is unbound in the notation.") | _ -> () +let check_binder_type recvars etyps = + let l1,l2 = List.split recvars in + let l = l1@l2 in + List.iter (function + | (x,ETBinder b) when not (List.mem x l) -> + errorlabstrm "" (str (if b then "binder" else "closed binder") ++ + strbrk " is only for use in recursive notations for binders.") + | _ -> ()) etyps + let not_a_syntax_modifier = function | SetOnlyParsing -> true | SetOnlyPrinting -> true @@ -1009,6 +1018,7 @@ let compute_syntax_data df modifiers = let toks = split_notation_string df in let (recvars,mainvars,symbols) = analyze_notation_tokens toks in let _ = check_useless_entry_types recvars mainvars etyps in + let _ = check_binder_type recvars etyps in let ntn_for_interp = make_notation_key symbols in let symbols' = remove_curly_brackets symbols in let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in |