diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-12 16:40:32 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:04 +0100 |
| commit | 433f0bc4e5110db09c770022b277c419f8b35f64 (patch) | |
| tree | 12f881fa7bbc72783dc2be9e7df7c39b05a7bbc7 /library/summary.mli | |
| parent | 5f2f22e7ff5d53e3258affa0e0e41666d5e0691d (diff) | |
Summary: more surgery functions
API to let one forge a frozen state out of another frozen state
plus some frozen bits
Diffstat (limited to 'library/summary.mli')
| -rw-r--r-- | library/summary.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/library/summary.mli b/library/summary.mli index 1ce09e12c..1dcb1d5f5 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -68,3 +68,6 @@ type frozen_bits val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits val unfreeze_summary : frozen_bits -> unit +val surgery_summary : frozen -> frozen_bits -> frozen +val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits +val pointer_equal : frozen_bits -> frozen_bits -> bool |