diff options
Diffstat (limited to 'grammar/tacextend.ml4')
| -rw-r--r-- | grammar/tacextend.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 2e725b46c3..70151cef1b 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -257,10 +257,10 @@ EXTEND ; tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name false None e "" in + let EntryName (t, g) = interp_entry_name false None e "" in GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = interp_entry_name false None e sep in + let EntryName (t, g) = interp_entry_name false None e sep in GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | s = STRING -> if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal."); |