diff options
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 54eed5ea6..f593b4547 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -40,6 +40,7 @@ val union_side_effects : side_effects -> side_effects -> side_effects val flatten_side_effects : side_effects list -> side_effects val side_effects_of_list : side_effect list -> side_effects val cons_side_effects : side_effect -> side_effects -> side_effects +val side_effects_is_empty : side_effects -> bool (** {6 Inductive types} *) |