diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-27 14:36:20 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-27 14:36:20 +0000 |
commit | caff708cff41f6bb91d26b59f3d93018f17f63ba (patch) | |
tree | 3bfaa5435af318cd32ab576a1eba24cb5dd3c715 /toplevel/metasyntax.ml | |
parent | 97f8b7f86e62ac84e644c982fb3407c38d2de5a9 (diff) |
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
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r-- | toplevel/metasyntax.ml | 6 |
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 |