diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-16 16:12:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-16 16:12:08 +0000 |
| commit | 42e084aae0d0a7fb1209dcbade3438cdde93f776 (patch) | |
| tree | 08010d3fda996d4023af119b3830deeb98514c3b /library | |
| parent | 6ec055d4ca1f728e6a357c9189f733efb82cdd78 (diff) | |
Déplacement/renommage de Class.stre_max en Declare.strength_min
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2648 85f007b7-540e-0410-9357-904b9bb8a0f7
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 a67260d01..6b2f9a6ae 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 c914245ff..b7b305cfa 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 |