diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e2932a904..8b47ced02 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -15,6 +15,7 @@ open Nameops open Sign open Term open Declarations +open Entries open Environ open Evd open Declare @@ -34,7 +35,7 @@ open Safe_typing type proof_topstate = { top_hyps : named_context * named_context; top_goal : goal; - top_strength : bool * Nametab.strength; + top_strength : bool * Libnames.strength; top_hook : declaration_hook } let proof_edits = |