diff options
| author | herbelin | 2007-03-15 16:34:29 +0000 |
|---|---|---|
| committer | herbelin | 2007-03-15 16:34:29 +0000 |
| commit | bda9e8da3320c3d54be356878c8d8cd9b3caec11 (patch) | |
| tree | 8f35caa28331b14c051552e44a85becbf765b3f6 | |
| parent | 2587079016467becd13b607c24212c16785456a3 (diff) | |
Prévention notations récursives sans terminal à gauche et qui font boucler
le parser
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9706 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 8876ce2119..855c98f93b 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -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 |