blob: fffe5834899634ccd6e8d353e01dc03da2433855 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(*i $Id$ i*)
open Proof_type
open Term
(* This module intends to be a beginning of debugger for tactic expressions.
Currently, it is quite simple and we can hope to have, in the future, a more
complete panel of commands dedicated to a proof assistant framework *)
(* Debug information *)
type debug_info =
| DebugOn
| DebugOff
| Exit
(* Prints the state and waits *)
val debug_prompt : goal sigma option -> Coqast.t -> debug_info
(* Prints a matched hypothesis *)
val db_matched_hyp : debug_info -> Environ.env -> string * constr -> unit
(* Prints the matched conclusion *)
val db_matched_concl : debug_info -> Environ.env -> constr -> unit
|
