diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index f3f6ab8e41..0ebf97a7bd 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -44,6 +44,8 @@ val red_set : reds -> red_kind -> bool (* Adds a reduction kind to a set *) val red_add : reds -> red_kind -> reds +(* Gives the constant list *) +val red_get_const : reds -> bool * (section_path list) (*s Reduction function specification. *) |