summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGabriel Kerneis2014-05-15 12:30:03 +0100
committerGabriel Kerneis2014-05-15 12:30:03 +0100
commitf12a48f09bc6bc44c8cac0de6f4ebb8ab2a14cb6 (patch)
tree20a0a437f9b965bddc136e9d31c86e30e035cd4c /src
parentfa39ead01f773e1967414ce421fdd86d476a96fe (diff)
Check name_sect during parsing
Diffstat (limited to 'src')
-rw-r--r--src/parser.mly5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/parser.mly b/src/parser.mly
index 50b2da34..76619f59 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1011,7 +1011,10 @@ typquant:
name_sect:
| Lsquare Id Eq String Rsquare
- { Name_sect_aux(Name_sect_some($4), loc ()) }
+ {
+ if $2 <> "name" then
+ raise (Parse_error_locn ((loc ()),"Unexpected id \""^$2^"\" in name_sect (should be \"name\")"));
+ Name_sect_aux(Name_sect_some($4), loc ()) }
c_def_body:
| typ id