diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 19:53:51 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-10 18:11:02 -0400 |
| commit | 39c4f9030f3aefdb7581aa02dd4b0c0d1ef89ee5 (patch) | |
| tree | 9489b19632ba418a6dd9ef047543851eb069ebd4 /kernel/safe_typing.mli | |
| parent | 91171386f55a2d423d831a1ce96f9d621a5be141 (diff) | |
[sideeff] Don't use polymorphic equality to check for empty side-effects
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f8d5d319a9..b42746a882 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants val empty_private_constants : private_constants +val is_empty_private_constants : private_constants -> bool + val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) |