diff options
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index a297f25868..df81291e7e 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -211,10 +211,6 @@ module Internal : sig (* Overriding opacity is indeed really hacky *) val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry - (* TODO: This is only used in DeclareDef to forward the fix to - hooks, should eventually go away *) - val get_fix_exn : 'a proof_entry -> Future.fix_exn - val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list type constant_obj |