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

3 files changed, 19 insertions, 29 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
diff --git a/toplevel/class.ml b/toplevel/class.ml
index d9500b11d5..3096b6067b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -24,31 +24,8 @@ open Declare
 open Nametab
 open Safe_typing
 
-(* manipulations concernant les strength *)
-
-(* gt dans le sens de "longueur du sp" (donc le moins persistant) *)
-
-(* strength * strength -> bool *)
-
-let stre_gt = function
-(*  | (x,y) when (x = NeverDischarge || x = NotDeclare)
-            && (y = NeverDischarge || y = NotDeclare) -> false
-  | (x,_) when x = NeverDischarge || x = NotDeclare -> false
-  | (_,x) when x = NeverDischarge || x = NotDeclare -> true*)
-
-  | (NeverDischarge,_) -> false
-  | (NotDeclare,_) -> false
-  | (_,NeverDischarge) -> true
-  | (_,NotDeclare) -> true
-  | (DischargeAt (sp1,_),DischargeAt (sp2,_)) ->
-      is_dirpath_prefix_of sp1 sp2
-	(* was sp_gt but don't understand why - HH *)
-
-let stre_max (stre1,stre2) =
-  if stre_gt (stre1,stre2) then stre1 else stre2
-
-let stre_max4 stre1 stre2 stre3 stre4 =
-  stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4)))
+let strength_min4 stre1 stre2 stre3 stre4 =
+  strength_min ((strength_min (stre1,stre2)),(strength_min (stre3,stre4)))
 
 let id_of_varid c = match kind_of_term c with
   | Var id -> id
@@ -67,7 +44,7 @@ let rec stre_unif_cond = function
       else
 	let stre1 = (variable_strength v1)
 	and stre2 = (variable_strength v2) in 
-	stre_max (stre1,stre2)
+	strength_min (stre1,stre2)
 
 (* Errors *)
 
@@ -137,7 +114,7 @@ let try_add_class cl streopt fail_if_exists =
     let p = check_arity cl in
     let stre' = strength_of_cl cl in 
     let stre = match streopt with
-      | Some stre -> stre_max (stre,stre')
+      | Some stre -> strength_min (stre,stre')
       | None -> stre'
     in
     declare_class (cl,stre,p)
@@ -235,8 +212,8 @@ let get_strength stre ref cls clt =
   let streunif = stre_unif_cond (s_vardep,f_vardep) in
  *)
   let streunif = NeverDischarge in
-  let stre' = stre_max4 stres stret stref streunif in
-  stre_max (stre,stre')
+  let stre' = strength_min4 stres stret stref streunif in
+  strength_min (stre,stre')
 
 (* coercion identité *)