diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 5cbfd4954..b58dc654d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -369,7 +369,7 @@ GEXTEND Gram | (false, _) -> <:ast< (CALL $id ($LIST $l)) >> | _ -> Util.user_err_loc (loc, "G_tactic.meta_tactic", - [< 'sTR"Cannot apply arguments to a meta-tactic." >]) + (str"Cannot apply arguments to a meta-tactic.")) ] *)] ; tactic: |