diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/library/declare.mli b/library/declare.mli index c914245ffd..b7b305cfa1 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -31,6 +31,9 @@ type strength = | DischargeAt of dir_path * int | NeverDischarge +val is_less_persistent_strength : strength * strength -> bool +val strength_min : strength * strength -> strength + type section_variable_entry = | SectionLocalDef of constr * types option | SectionLocalAssum of types |