diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 0ea59eea2..cd63d419e 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -93,7 +93,7 @@ val suspend_proof : unit -> unit into a constant with its name and strength; it fails if there is no current proof of if it is not completed *) -val cook_proof : unit -> identifier * (Declarations.constant_entry * strength) +val cook_proof : unit -> identifier * (Safe_typing.constant_entry * strength) (*s [get_pftreestate ()] returns the current focused pending proof or raises [UserError "no focused proof"] *) |