aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.mli')
-rw-r--r--toplevel/vernacentries.mli5
1 files changed, 5 insertions, 0 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 451ccdb4d..4e7fa4a08 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -59,3 +59,8 @@ val vernac_end_proof :
?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
val with_fail : bool -> (unit -> unit) -> unit
+
+val command_focus : unit Proof.focus_kind
+
+val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr ->
+ Evd.evar_map * Redexpr.red_expr) Hook.t