don't require printing-only notation to be productive

1 files changed, 7 insertions, 6 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 008d5cf9f..ccb9c99d7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -903,8 +903,8 @@ let find_precedence lev etyps symbols =
   let first_symbol =
     let rec aux = function
       | Break _ :: t -> aux t
-      | h :: t -> h
-      | [] -> assert false (* rule is known to be productive *) in
+      | h :: t -> Some h
+      | [] -> None in
     aux symbols in
   let last_is_terminal () =
     let rec aux b = function
@@ -914,7 +914,8 @@ let find_precedence lev etyps symbols =
       | [] -> b in
     aux false symbols in
   match first_symbol with
-  | NonTerminal x ->
+  | None -> [],0
+  | Some (NonTerminal x) ->
       (try match List.assoc x etyps with
 	| ETConstr _ ->
 	    error "The level of the leftmost non-terminal cannot be changed."
@@ -937,11 +938,11 @@ let find_precedence lev etyps symbols =
 	if Option.is_empty lev then
 	  error "A left-recursive notation must have an explicit level."
 	else [],Option.get lev)
-  | Terminal _ when last_is_terminal () ->
+  | Some (Terminal _) when last_is_terminal () ->
       if Option.is_empty lev then
 	([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
-  | _ ->
+  | Some _ ->
       if Option.is_empty lev then error "Cannot determine the level.";
       [],Option.get lev
 
@@ -991,7 +992,7 @@ let compute_syntax_data df modifiers =
   let symbols' = remove_curly_brackets symbols in
   let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in
   let ntn_for_grammar = make_notation_key symbols' in
-  check_rule_productivity symbols';
+  if not onlyprint then check_rule_productivity symbols';
   let msgs,n = find_precedence n etyps symbols' in
   let innerlevel = NumLevel 200 in
   let typs =