diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 10 | ||||
| -rw-r--r-- | library/declare.mli | 3 |
2 files changed, 13 insertions, 0 deletions
diff --git a/library/declare.ml b/library/declare.ml index a67260d01b..6b2f9a6ae3 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -62,6 +62,16 @@ let make_strength_2 () = if depth > 2 then DischargeAt (extract_dirpath_prefix 2 cwd, depth-2) else NeverDischarge +let is_less_persistent_strength = function + | (NeverDischarge,_) -> false + | (NotDeclare,_) -> false + | (_,NeverDischarge) -> true + | (_,NotDeclare) -> true + | (DischargeAt (sp1,_),DischargeAt (sp2,_)) -> + is_dirpath_prefix_of sp1 sp2 + +let strength_min (stre1,stre2) = + if is_less_persistent_strength (stre1,stre2) then stre1 else stre2 (* Section variables. *) 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 |