diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 8fbab3ca1..d3c9e6bb6 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -773,8 +773,8 @@ and intern_tacarg strict onlytac ist = function (match Dyn.tag t with | "tactic" | "value" -> x | "constr" -> if onlytac then error_tactic_expected loc else x - | s -> anomaly_loc (loc, "", - str "Unknown dynamic: <" ++ str s ++ str ">")) + | s -> anomaly ~loc + (str "Unknown dynamic: <" ++ str s ++ str ">")) (* Reads the rules of a Match Context or a Match *) and intern_match_rule onlytac ist = function |