aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r--proofs/proof_global.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 63bc4a7080..071858cd33 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -66,7 +66,7 @@ type lemma_possible_guards = int list list
type proof_info = {
strength : Decl_kinds.goal_kind ;
compute_guard : lemma_possible_guards;
- hook :Tacexpr.declaration_hook ;
+ hook : unit Tacexpr.declaration_hook ;
mode : proof_mode
}