diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index aa9ab17aa..fb3039c0e 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -25,11 +25,11 @@ let (grammar_state : grammar_command list ref) = ref [] let specify_name name e = match e with | UserError(lab,strm) -> - UserError(lab, [< 'sTR"during interpretation of grammar rule "; - 'sTR name; 'sTR","; 'sPC; strm >]) + UserError(lab, (str"during interpretation of grammar rule " ++ + str name ++ str"," ++ spc () ++ strm)) | Anomaly(lab,strm) -> - Anomaly(lab, [< 'sTR"during interpretation of grammar rule "; - 'sTR name; 'sTR","; 'sPC; strm >]) + Anomaly(lab, (str"during interpretation of grammar rule " ++ + str name ++ str"," ++ spc () ++ strm)) | Failure s -> Failure("during interpretation of grammar rule "^name^", "^s) | e -> e |