diff options
| author | herbelin | 2003-04-29 18:30:35 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-29 18:30:35 +0000 |
| commit | 0d0dd206eb2900f714838c96cc88eb9b8012fc30 (patch) | |
| tree | d7101ebe3ba9323d5f50b98af3b5d6496b88ac29 | |
| parent | 66eed5340efdfbd41a775cf679213507bb2ac424 (diff) | |
Prise en compte des syntaxes v8 dans Uninterpreted Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3984 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 19a03a22e6..4c62250d23 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -693,7 +693,7 @@ GEXTEND Gram | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (local,s,l) + -> VernacSyntaxExtension (local,s,l,None) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) |