From bf1e15181a2531a106fa643ca8e9233cb889af12 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Nov 2019 21:49:47 +0100
Subject: Fixes #4690: do not allow @f in notations when f is a notation
 variable.

---
 interp/constrintern.ml     | 9 +++++++++
 test-suite/bugs/bug_4690.v | 3 +++
 2 files changed, 12 insertions(+)
 create mode 100644 test-suite/bugs/bug_4690.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f68f4e67b9..c39e61083d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -637,6 +637,14 @@ let rec expand_binders ?loc mk bl c =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
+let check_not_notation_variable f ntnvars =
+  (* Check bug #4690 *)
+  match DAst.get f with
+  | GVar id when Id.Map.mem id ntnvars ->
+    user_err (str "Prefix @ is not applicable to notation variables.")
+  | _ ->
+     ()
+
 let option_mem_assoc id = function
   | Some (id',c) -> Id.equal id id'
   | None -> false
@@ -2063,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
             lvar us args ref
         in
+        check_not_notation_variable f ntnvars;
         (* Rem: GApp(_,f,[]) stands for @f *)
         if args = [] then DAst.make ?loc @@ GApp (f,[]) else
           smart_gapp f loc (intern_args env args_scopes (List.map fst args))
diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/bug_4690.v
new file mode 100644
index 0000000000..f50866a990
--- /dev/null
+++ b/test-suite/bugs/bug_4690.v
@@ -0,0 +1,3 @@
+(* Check that @f is not allowed in notation when f is a notation variable *)
+
+Fail Notation "# g" := (@g O) (at level 0).
-- 
cgit v1.2.3