diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-28 10:06:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-28 10:06:04 +0000 |
| commit | 31d6b27e29479b0082dfba5a1211f622c9e4111d (patch) | |
| tree | d9b8db31e79b26448852443b1b4336db0dc2ed5e | |
| parent | a2ad1a21e99555490fb23c18e1fcec1f28502ab3 (diff) | |
Correction bug #776
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5839 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a3415cbaa..bd45fb2d5 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -410,7 +410,8 @@ let rec find_pattern xl = function error ("The token "^s^" occurs on one side of \"..\" but not on the other side") | [NonTerminal _], Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side") - | ((SProdList _ | NonTerminal _) :: _ | []), _ -> assert false + | ((SProdList _ | NonTerminal _) :: _ | []), _ -> + error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\"") let rec interp_list_parser hd = function | [] -> [], List.rev hd |