diff options
| author | Maxime Dénès | 2017-06-15 21:54:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-15 21:54:34 +0200 |
| commit | 9beec0fc6cc283294bbbda363a3f788ae56347d5 (patch) | |
| tree | 2df172ba10cedaa935460eed511a9dc494d1bafa /API/API.mli | |
| parent | 5b109c098a46e5083ba0cf98b5fe72312331770e (diff) | |
| parent | 63896b2443e71e47c016fc9d0709cc22cf24f288 (diff) | |
Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 68fbda7c73..4b2845443e 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2694,7 +2694,6 @@ module Lib : sig | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list |