diff options
| author | herbelin | 2005-06-04 10:23:46 +0000 |
|---|---|---|
| committer | herbelin | 2005-06-04 10:23:46 +0000 |
| commit | 24e5510bfcd33049cbb1a1c709e93346f63bdd91 (patch) | |
| tree | 9a01519d87a2d7bf473d96c997649c3874c910b9 | |
| parent | 57e39940a20d7aaf8b1378daa68e06653ef10756 (diff) | |
Ajout explicite du niveau 200 de pattern auquel on fait référence au niveau 0; nécessaire pour option -nois
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7109 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_constrnew.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 5048b6bd86..99c3570f32 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -286,7 +286,8 @@ GEXTEND Gram [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ] ; pattern: - [ "100" LEFTA + [ "200" RIGHTA [ ] + | "100" LEFTA [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ] | "10" LEFTA [ p = pattern; lp = LIST1 (pattern LEVEL "0") -> |