Fixed bug #2967 (some missing check on ill-formed recursive notation strings).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16155 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 1 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f9721e2d8..60d600ca1 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -306,6 +306,9 @@ let split_notation_string str =
 
 let out_nt = function NonTerminal x -> x | _ -> assert false
 
+let msg_expected_form_of_recursive_notation =
+  "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
+
 let rec find_pattern nt xl = function
   | Break n as x :: l, Break n' :: l' when Int.equal n n' ->
       find_pattern nt (x::xl) (l,l')
@@ -318,13 +321,14 @@ let rec find_pattern nt xl = function
   | _, Terminal s :: _ | Terminal s :: _, _ ->
       error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
-      error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
+      error msg_expected_form_of_recursive_notation
   | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
       anomaly "Only Terminal or Break expected on left, non-SProdList on right"
 
 let rec interp_list_parser hd = function
   | [] -> [], List.rev hd
   | NonTerminal id :: tl when Id.equal id ldots_var ->
+      if List.is_empty hd then error msg_expected_form_of_recursive_notation;
       let hd = List.rev hd in
       let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
       let xyl,tl'' = interp_list_parser [] tl' in