diff options
| author | Pierre-Marie Pédrot | 2016-03-21 00:19:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-21 00:19:40 +0100 |
| commit | df6132c06f9c8480b01f0a269cd1b95bbaa7f912 (patch) | |
| tree | 9260ceec0d4824c617bfad79b0d1953c5b971fd7 /tactics/tactic_debug.mli | |
| parent | 6afe572a4448e50f18e408097dd9ed03cc432d39 (diff) | |
| parent | 87e27056beee0f7b63326d0a1cb3f68249539bee (diff) | |
Moving the last parts of the Ltac engine to hightactics.
Diffstat (limited to 'tactics/tactic_debug.mli')
| -rw-r--r-- | tactics/tactic_debug.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli index 523398e75a..520fb41eff 100644 --- a/tactics/tactic_debug.mli +++ b/tactics/tactic_debug.mli @@ -61,13 +61,13 @@ val db_matching_failure : debug_info -> unit Proofview.NonLogical.t val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t (** An exception handler *) -val explain_logic_error: (exn -> Pp.std_ppcmds) ref +val explain_logic_error: exn -> Pp.std_ppcmds (** For use in the Ltac debugger: some exception that are usually consider anomalies are acceptable because they are caught later in the process that is being debugged. One should not require from users that they report these anomalies. *) -val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref +val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds (** Prints a logic failure message for a rule *) val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t |