aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8b47ced02..a3e18f150 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -35,7 +35,7 @@ open Safe_typing
type proof_topstate = {
top_hyps : named_context * named_context;
top_goal : goal;
- top_strength : bool * Libnames.strength;
+ top_strength : Decl_kinds.goal_kind;
top_hook : declaration_hook }
let proof_edits =