diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
| commit | 4767d724d489a7ad67f696e9401e70b9f9ae2143 (patch) | |
| tree | 142a99bc1cd3beef403f1942908de090f70c5e07 /toplevel/metasyntax.ml | |
| parent | 72b9a7df489ea47b3e5470741fd39f6100d31676 (diff) | |
Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 3dcb1f58..13f1f1da 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 9333 2006-11-02 13:59:14Z barras $ *) +(* $Id: metasyntax.ml 10192 2007-10-08 00:33:39Z letouzey $ *) open Pp open Util @@ -28,7 +28,7 @@ open Notation (**********************************************************************) (* Tokens *) -let cache_token (_,s) = Pcoq.lexer.Token.using ("", s) +let cache_token (_,s) = Compat.using Pcoq.lexer ("", s) let (inToken, outToken) = declare_object {(default_object "TOKEN") with @@ -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 |