blob: 26ab1a9470aeae30fffc5e55a0edf904c23c5e49 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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
|
