From 727ef1bd345f9ad9e08d9e4f136e2db7d034a93d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Apr 2017 22:35:38 +0200
Subject: Fixing bug #5470 (anomaly on notations with misused "binder" type).

---
 test-suite/bugs/closed/5470.v |  3 +++
 toplevel/metasyntax.ml        | 10 ++++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/5470.v

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
-- 
cgit v1.2.3