diff options
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 8876ce2119..855c98f93b 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -739,7 +739,9 @@ let set_entry_type etyps (x,typ) = let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then - error "A notation must include at least one symbol" + error "A notation must include at least one symbol"; + if (match l with SProdList _ :: _ -> true | _ -> false) then + error "A recursive notation must start with at least one symbol" let is_not_printable = function | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true |