aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.mli')
-rw-r--r--toplevel/vernacentries.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 814676575d..8fb6f4668c 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -39,7 +39,7 @@ type pcoq_hook = {
print_check : Environ.env -> Environ.unsafe_judgment -> unit;
print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
Environ.unsafe_judgment -> unit;
- show_goal : int option -> unit
+ show_goal : goal_reference -> unit
}
val set_pcoq_hook : pcoq_hook -> unit