diff options
| author | Emilio Jesus Gallego Arias | 2020-04-21 13:45:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 18:05:14 +0200 |
| commit | ad84e6948a86db491a00bb92ec3e00a9a743b1f9 (patch) | |
| tree | 7a85b4dfe31bfc26b97baaa6acd306e9ff144bb8 /vernac/declare.mli | |
| parent | e4bfbdfc4b4944d6e6d702eb732bce24f962e67f (diff) | |
[declare] Remove fix_exn internal access.
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 |