diff options
Diffstat (limited to 'proofs/tactic_debug.mli')
| -rw-r--r-- | proofs/tactic_debug.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index aa386762b9..4a6aecfde9 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -24,6 +24,9 @@ type debug_info = (* Prints the state and waits *) val debug_prompt : goal sigma option -> Coqast.t -> debug_info +(* Prints a constr *) +val db_constr : debug_info -> Environ.env -> constr -> unit + (* Prints a matched hypothesis *) val db_matched_hyp : debug_info -> Environ.env -> string * constr -> unit |