Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).

This fixes also #9640 part 1.

3 files changed, 52 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/bug_9521.v b/test-suite/bugs/closed/bug_9521.v
new file mode 100644
index 0000000000..0464c62c09
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9521.v
@@ -0,0 +1,23 @@
+(* Example from #9521 *)
+
+Module A.
+
+Declare Custom Entry expr.
+Notation "expr0:( s )" := s (s custom expr at level 0).
+Notation "#" := 0 (in custom expr at level 1).
+Check expr0:(#). (* Should not be an anomaly "unknown level 0" *)
+
+End A.
+
+(* Another example from a comment at #11561 *)
+
+Module B.
+
+Declare Custom Entry special.
+Declare Custom Entry expr.
+Notation "## x" := (S x) (in custom expr at level 10, x custom special at level 10).
+Notation "[ e ]" := e (e custom expr at level 10).
+Notation "1" := 1 (in custom special).
+Check [ ## 1 ].
+
+End B.
diff --git a/test-suite/bugs/closed/bug_9640.v b/test-suite/bugs/closed/bug_9640.v
new file mode 100644
index 0000000000..4dc0bead7b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9640.v
@@ -0,0 +1,23 @@
+(* Similar to #9521 (was an anomaly unknown level 150 *)
+
+Module A.
+
+Declare Custom Entry expr.
+Notation "p" := (p) (in custom expr at level 150, p constr, right associativity).
+Notation "** X" := (X) (at level 200, X custom expr at level 150).
+Lemma t : ** True.
+Abort.
+
+End A.
+
+(* Similar to #9517, #9519, #11331 *)
+
+Module B.
+
+Declare Custom Entry expr.
+Notation "p" := (p) (in custom expr at level 100, p constr (* at level 200 *)).
+Notation "** X" := (X) (at level 200, X custom expr at level 150).
+Lemma t : ** True.
+Abort.
+
+End B.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 9f41287bce..3181bcc4bc 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -507,13 +507,18 @@ let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
   let empty = (pos, [(name, p4assoc, [])]) in
   ExtendRule (target_entry where forpat, reinit, empty)
 
+let different_levels (custom,opt_level) (custom',string_level) =
+  match opt_level with
+  | None -> true
+  | Some level -> not (Notation.notation_entry_eq custom custom') || level <> int_of_string string_level
+
 let rec pure_sublevels' assoc from forpat level = function
 | [] -> []
 | GramConstrNonTerminal (e,_) :: rem ->
    let rem = pure_sublevels' assoc from forpat level rem in
    let push where p rem =
      match symbol_of_target where p assoc from forpat with
-     | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+     | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem
      | _ -> rem in
    (match e with
    | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem