Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations

4 files changed, 22 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 08c609cfa..39f119e7c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,8 @@ Notations
 
 - Recursive notations with the recursive pattern repeating on the
   right (e.g. "( x ; .. ; y ; z )") now supported.
+- Notations with a specific level for the leftmost nonterminal,
+  when printing-only, are supported.
 
 Tactics
 
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 65efe228a..6ef75dd13 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -124,3 +124,7 @@ return (1, 2, 3, 4)
      : nat
 !!! _ _ : nat, True
      : (nat -> Prop) * ((nat -> Prop) * Prop)
+((*1).2).3
+     : nat
+*(1.2)
+     : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ea372ad1a..8c7bbe591 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -190,3 +190,10 @@ Check 1+1+1.
 (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
 Check !!! (x y:nat), True.
+
+(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
+
+Notation "* x" := (id x) (only printing, at level 15, format "* x").
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 5298ef2e4..b2d48bb2f 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -991,7 +991,7 @@ let is_not_printable onlyparse nonreversible = function
      (warn_non_reversible_notation (); true)
   else onlyparse
 
-let find_precedence lev etyps symbols =
+let find_precedence lev etyps symbols onlyprint =
   let first_symbol =
     let rec aux = function
       | Break _ :: t -> aux t
@@ -1009,8 +1009,13 @@ let find_precedence lev etyps symbols =
   | None -> [],0
   | Some (NonTerminal x) ->
       (try match List.assoc x etyps with
-	| ETConstr _ ->
-	    user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
+        | ETConstr _ ->
+	   if onlyprint then
+	     if Option.is_empty lev then
+	       user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.")
+	     else [],Option.get lev
+	   else
+	     user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
 	| ETName | ETBigint | ETReference ->
             begin match lev with
             | None ->
@@ -1134,7 +1139,7 @@ let compute_syntax_data df modifiers =
   let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
   let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in
   if not onlyprint then check_rule_productivity symbols_for_grammar;
-  let msgs,n = find_precedence mods.level mods.etyps symbols in
+  let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in
   (* To globalize... *)
   let etyps = join_auxiliary_recursive_types recvars mods.etyps in
   let sy_typs, prec =