diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2entries.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 2a0c109a42..2820d3e3ad 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -862,7 +862,7 @@ let () = CErrors.register_additional_error_info begin fun info -> let bt = str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt ++ fnl () in - Some (Loc.tag @@ Some bt) + Some (Loc.tag bt) else None end |