diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 23:54:55 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:27 +0200 |
commit | 58630ad9a0b94a804a39a3d99f982965292692c7 (patch) | |
tree | 0adadc2828cfeeaf122bf6086990997c8b72f2c1 /plugins/ltac/tactic_debug.mli | |
parent | 9367f1626afb080d10d425262dca705046a32933 (diff) |
[api] Misctypes removal: miscellaneous aliases.
Diffstat (limited to 'plugins/ltac/tactic_debug.mli')
-rw-r--r-- | plugins/ltac/tactic_debug.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 734e76b56..175341df0 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -76,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - Misctypes.lident message_token list -> unit Proofview.NonLogical.t + lident message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located |