From 31d6b27e29479b0082dfba5a1211f622c9e4111d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 28 Jun 2004 10:06:04 +0000
Subject: Correction bug #776

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5839 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3